# HG changeset patch # User wenzelm # Date 1401958440 -7200 # Node ID 550b704d665e03c786dd9c78dcb813e236f3e5a4 # Parent da107539996fd0dd8fdeac04c66978d91bf5b8e5 more on Query panel -- updated Find Theorems; diff -r da107539996f -r 550b704d665e 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} *}