search

ggrov / tinker

Graph based proof strategy language
http://ggrov.github.io/tinker/
6 stars 0 forks source link

aggressive error messages when atomic tactics not existing #60

Closed ggrov closed 8 years ago

ggrov commented 9 years ago

The error messages when I introduce an atomic tactic is very aggressive - e.g. I cannot even delete a node if the atomic method does not exists as all that happens is I get the error message again. Fine to have a warning when it first introduced but that should be it - e.g. what if I wanted to add it later but draw the graph first?. Maybe we could just have a red font for this case (or scribbled underscore as in Eclipse)?

plebras commented 9 years ago

That should actually have been fixed. Although it is probably not in the build yet. I will check that.