src/Doc/JEdit/JEdit.thy

--- a/src/Doc/JEdit/JEdit.thy	Wed Jun 04 18:18:09 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Thu Jun 05 10:54:00 2014 +0200
@@ -373,7 +373,7 @@
   or disprovers in the background). *}
 
 
-section {* Prover output \label{sec:prover-output} *}
+section {* Output \label{sec:prover-output} *}
 
 text {* Prover output consists of \emph{markup} and \emph{messages}.
   Both are directly attached to the corresponding positions in the
@@ -447,6 +447,82 @@
   \secref{sec:sledgehammer}).  *}
 
 
+section {* Query \label{sec:query} *}
+
+text {*
+  The \emph{Query} panel provides various GUI forms to request extra
+  information from the prover explicitly. In old times the user would have
+  issued some diagnostic command like @{command find_theorems} and inspected
+  its output, but this is now integrated more directly into the Prover IDE.
+
+  A \emph{Query} window provides some input fields and buttons for a
+  particular query command, with output in a dedicated text area. There are
+  various query modes: \emph{Find Theorems}, \emph{Find Constants},
+  \emph{Print Context}. As usual in jEdit, multiple \emph{Query} windows may
+  be active simultaneously: any number of floating instances, but at most one
+  docked instance (which is used by default).
+
+  \medskip The following GUI elements are common to all modes of query:
+  \begin{itemize}
+
+  \item The spinning wheel provides feedback about the status of a pending
+  query wrt.\ the evaluation of its context and its own operation.
+
+  \item The \emph{Apply} button attaches a fresh query invocation to the
+  current context of the command where the cursor is pointing in the text.
+
+  \item The \emph{Search} field allows to highlight query output according to
+  some regular expression. This may serve as an additional visual filter of
+  the result.
+
+  \item The \emph{Zoom} box controls the font size of the output area.
+
+  \end{itemize}
+
+  All query operations are asynchronous: there is no need to wait for the
+  evaluation of the document for the query context, nor for the query
+  operation itself. Query output may be detached as independent \emph{Info}
+  window, using a menu operation of the dockable window manager. The printed
+  result usually provides sufficient clues about the original query, with some
+  hyperlink to its context (via markup of its head line).
+*}
+
+
+subsection {* Find theorems *}
+
+text {*
+  The \emph{Query} panel in \emph{Find Theorems} mode
+  (\figref{fig:find-theorems}) provides access to the Isar command @{command
+  find_theorems}, using some GUI elements instead of command-line arguments.
+  The main text field accepts search criteria according to the syntax @{syntax
+  thmcriterium} given in \cite{isabelle-isar-ref}. Some further options of
+  @{command find_theorems} are available via GUI elements.
+
+  % FIXME update
+  \begin{figure}[htb]
+  \begin{center}
+  \includegraphics[scale=0.3]{find}
+  \end{center}
+  \caption{An instance of the Find panel}
+  \label{fig:find-theorems}
+  \end{figure}
+*}
+
+
+subsection {* Find constants *}
+
+text {*
+  FIXME
+*}
+
+
+subsection {* Print context *}
+
+text {*
+  FIXME
+*}
+
+
 section {* Tooltips and hyperlinks \label{sec:tooltips-hyperlinks} *}
 
 text {*
@@ -553,11 +629,11 @@
   Replacement text is inserted immediately into the buffer, unless
   ambiguous results demand an explicit popup.
 
-  \paragraph{Implicit completion} is triggered by regular keyboard
-  input events during of the editing process in the main jEdit text
-  area (and a few additional text fields like the search criteria of
-  the Find panel, see \secref{sec:find}).  Implicit completion depends
-  on on further side-conditions:
+  \paragraph{Implicit completion} is triggered by regular keyboard input
+  events during of the editing process in the main jEdit text area (and a few
+  additional text fields like the ones of the the \emph{Query} panel, see
+  \secref{sec:query}). Implicit completion depends on on further
+  side-conditions:
 
   \begin{enumerate}
 
@@ -897,28 +973,6 @@
   nonetheless, say to remove earlier proof attempts. *}
 
 
-section {* Find theorems \label{sec:find} *}
-
-text {* The \emph{Find} panel (\figref{fig:find}) provides an
-  independent view for the Isar command @{command find_theorems}.  The
-  main text field accepts search criteria according to the syntax
-  @{syntax thmcriterium} given in \cite{isabelle-isar-ref}.  Further
-  options of @{command find_theorems} are available via GUI elements.
-
-  \begin{figure}[htb]
-  \begin{center}
-  \includegraphics[scale=0.3]{find}
-  \end{center}
-  \caption{An instance of the Find panel}
-  \label{fig:find}
-  \end{figure}
-
-  The \emph{Apply} button attaches a fresh invocation of @{command
-  find_theorems} to the current context of the command where the
-  cursor is pointing in the text, unless an alternative theory context
-  (from the underlying logic image) is specified explicitly. *}
-
-
 chapter {* Miscellaneous tools *}
 
 section {* SideKick \label{sec:sidekick} *}