Execute Current Tactic picks up multiple tactics in one line

[aqjune]

Hi,

'Execute Current Tactic' can pick up multiple tactics if they are concatenated by THEN in one line, but this behavior seems a bit less intuitive because to me it feels like it is supposed to pick up only one tactic:

(*cursor here*) REWRITE_TAC[] THEN STRIP_TAC THEN
(* If I do 'Execute Current Tactic', it runs both of the tactics *)

Do you have a plan to support this more fine-grained behavior? It seems 'Execute Current Tactic (Multiple Lines)' works similarly.

One side note is do we need to have two different features - 'Execute Current Tactic (Multiple Lines)' and 'Execute Current Tactic'? Actually I found that I mostly use the former one. :) Wondering what was the motivation behind having the two features.

[monadius]

The Execute Current Tactic behavior is the same as in the existing Emacs mode for HOL Light: It executes the current line (or the current selection) in a REPL as a tactic. Initially, only this command for sending tactics to REPL was implemented. But then I observed that many tactics occupy several lines and implemented the multi-line version of this command. I agree that the multi-line version of this command is more useful.

It makes sense to update the Execute Current Tactic command to execute a single tactic at the cursor position (similar to how commands are executed with Send current statement to REPL). I will work on this change. Hopefully, it does not create any inconvenience for those who used to the Alt + L shortcut.

[aqjune]

Yeah, I vote for changing the default behavior of Execute Current Tactic as well as its multiline version to select a single tactic even if there are more than one tactic in the line. I think this is also consistent with other proof assistant IDEs such as CoqIde. :)

Another independent tiny bug that I've found was when a tactic was finishing with ;, for example:

... THENL
[A_TAC; B_TAC]

In this case, more than one tactic is picked up.