LS-Lab / KeYmaeraX-release

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
http://keymaeraX.org/
GNU General Public License v2.0
75 stars 37 forks source link

[Usability enhancement] Deleting text in tactic window leads to incorrect underlining #80

Closed rbohrer closed 2 years ago

rbohrer commented 3 years ago

When I first start by proof and it has "nil" in the tactic window, I'll often delete "nil" and paste a tactic script over it, out of force of habit. KeYmaera X gets confused because I deleted 3 characters, so it will delete 3 characters from my tactic when deciding what to underline/parse/attempt to run.

Low-priority because obvious fix is to just not delete it. Though one small awkwardness is that the tactic window will only parse your tactic when you type in something that shouldn't parse, by which I mean, if I write

nil auto

that's a syntax error because there's no ; between them, but if I add the ; then

nil ; auto

will not parse because the tactic interpreter tries to run "; auto" which is not a tactic

non-blocking for experienced users but could definitely surprise newbies

smitsch commented 2 years ago

Fixed with tactic editor updates in v4.9.8