[isabelle-dev] jedit

[Lawrence Paulson]

You seem to be saying that the main difficulty with providing menus is that they would insert material into the proof script. My own feeling is, if this is the only way we can have menus, then so be it: without them, we still have to type in the very same material.

A quirk of the current setup is that typing “sledgehammer" has no effect; you have to explicitly move the cursor after this keyword before sledgehammer launches. A menu would solve this problem as well.

Larry

On 16 May 2012, at 12:51, Makarius wrote:

> Conceptually, there is a deeper reason why such things outside the main editor buffer are not yet supported: the document model is based on explicit edits and corresponding changes of the semantic content.  There is simply no support yet for diagnostic functions over existing document content.  One needs to simulate that by editing the query functions into the text, presently by manual editing. Moreover, many of the PG menu operations are actually changing global state variables in the prover process, which is incompatible with the asynchronous editor model.