[isabelle-dev] NEWS: "Query" panel supersedes "Find"

Makarius makarius at sketis.net
Wed May 7 15:19:36 CEST 2014


* 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


More information about the isabelle-dev mailing list