HOL-Theorem-Prover
Parse strings in HOL to execute editor actions
Currently all the different editor modes have different approaches on the editor side to automatically process or trim a selection of the text buffer to make it suitable to pass as code to e.g. a function in proofManagerLib. This work can be done in a proper and standardised way once-and-for-all in HOL with a string -> unit interface that lets the editors focus on the much simpler task of piping text to HOL.
Example of the kind of work that's done differently in each editor mode: trimming THEN (and synonyms like >>) from the start and end of tactics.
In Moscow ML, this code will need to use use. The parsing code can be kept separate, but the final stage that invokes use to apply the tactic (evaluate the region, ...) will need to live in std.prelude because that's the only place where we can put such code. (Moscow ML won't compile code that calls use.)
