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

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to