Re: [isabelle] »strict« or »sequential« mode in Isabelle/jEdit?



On Tue, 22 Apr 2014, Makarius wrote:

The deep path through the GUI can be avoided by mapping the jEdit action "plugin-options" to some key that is still free on your keyboard. That depends on many individual side-conditions and it is common practice for jEdit plugins to provide default key bindings rarely.

Here are some more possibilities for quick access to jEdit actions:

  * The toolbar, which is off by default in Isabelle/jEdit.  The menu
    "Global Options / Tool Bar" allows to enable it and edit its entries.
    In the next release that will be there by default, because the
    Navigator needs it for forward / backward icons.

  * The context menu, which shows up on a right-click on the text area.
    See "Global Options / Context Menu" or its last item to edit it
    in-place.  The menu popup might get into conflict with Isabelle/jEdit
    tooltips or completion popups -- this will be more smooth in the next
    release.

  * There is also a mini command-line for actions available via C-RETURN,
    which has its own TAB-completion.  Its popup window is the default one
    of jEdit, which has some platform-specific problems on Mac OS X and a
    few Linux systems, but it should work under "normal" circumstances.

In any case the critical bit is the "action" to be invoked. I usually try to provide Isabelle/jEdit actions as far as I can make sense of them. If there is anything missing, just tell me about it.

Alternatively, it might be possible to let BeanShell invoke some functionality under script control, but that could be difficult to access, because Scala is not Java.


These advanced concepts are actually common-place from the regular jEdit standpoint. Since some people still call Isabelle/jEdit wrongly "jEdit", and don't really know jEdit itself, the next release will provide direct access to the jEdit documentation. Presently there is just an URL in Isabelle/jEdit manual section 1.2.1 Documentation.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.