[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Mon May 12 14:46:07 CEST 2014
On Fri, 2 May 2014, Makarius wrote:
> On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
> Until then there are various approximations:
> * Multiple floating instances of Output, with different Update / Auto
> update state.
> * The Output / Detach button to produce an unchanging Info window on the
In Isabelle/c2ddbf327bbd the former "Detach" button is now a menu item in
all dockable windows that support this concept of producing a stand-alone
"Info" window from a snapshot of the content.
Since "Query" and "Info" already do a good job for keeping track of
invididual state output, outside the auto-update mode of Output, I was
wondering if it is time to *discontinue* its special buttons:
Output / Update
Output / Auto update
These are remains from early experimental generations of Isabelle/jEdit
some years ago. Is anyone actually using that in current repository
versions, not the last release?
Since former Proof General and Emacs users often prefer keyboard over
mouse, the following standard jEdit actions might be interesting:
They are bound by default to Emacs-style multi key sequences, e.g.
In fact, the similarity to C+e DOWN for subscript in Isabelle/jEdit has
already caused some confusion to someone trying the latter, and not
knowing about Emacs ways to treat keyboards. Thus I learned about the
existance of the other key sequence in the first place, but also that
Emacs usage cannot be expected from regular users today.
More information about the isabelle-dev