[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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
>     spot.

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:

   left-docking-area
   right-docking-area
   top-docking-area
   bottom-docking-area

   close-docking-area

They are bound by default to Emacs-style multi key sequences, e.g.
C+e C+DOWN.

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.


       Makarius