* More general "Query" panel supersedes "Find" panel, with GUI access
to commands 'find_theorems' and 'find_consts', as well as print
operations for the context. Minor incompatibility in keyboard
shortcuts etc.: replace action isabelle-find by isabelle-query.
This refers to Isabelle/ee2b61f37ad9.
The ranaming was first motivated by the addition of various "print"
operations to query the context, which are not subsumed by "find". I see
more general principles emerging, though.
* "Output": spontaneous output that is implicitly produced by the
system.
* "Preview" (unimplemented): structured preview of the continously
checked document.
* "Query": extra information that is explicitly requested by the user.
The alphabetic proximity of all three dockables means that the jEdit
window manager will put the panels side-by-side, if they are in the same
margin of the editor view.
The GUI of "Query" has only seen two rounds of refinement so far. (I am a
bit concerned about the many fields and buttons.)
Note that it is also possible to query a proof state, and then work with
it independently of the proactive moves of "Output". The "Detach" button
is now uniformly available.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
