449 |
449 |
450 section {* Query \label{sec:query} *} |
450 section {* Query \label{sec:query} *} |
451 |
451 |
452 text {* |
452 text {* |
453 The \emph{Query} panel provides various GUI forms to request extra |
453 The \emph{Query} panel provides various GUI forms to request extra |
454 information from the prover explicitly. In old times the user would have |
454 information from the prover In old times the user would have issued some |
455 issued some diagnostic command like @{command find_theorems} and inspected |
455 diagnostic command like @{command find_theorems} and inspected its output, |
456 its output, but this is now integrated more directly into the Prover IDE. |
456 but this is now integrated into the Prover IDE. |
457 |
457 |
458 A \emph{Query} window provides some input fields and buttons for a |
458 A \emph{Query} window provides some input fields and buttons for a |
459 particular query command, with output in a dedicated text area. There are |
459 particular query command, with output in a dedicated text area. There are |
460 various query modes: \emph{Find Theorems}, \emph{Find Constants}, |
460 various query modes: \emph{Find Theorems}, \emph{Find Constants}, |
461 \emph{Print Context}, see also \figref{fig:query}. As usual in jEdit, |
461 \emph{Print Context}, e.g.\ see \figref{fig:query}. As usual in jEdit, |
462 multiple \emph{Query} windows may be active simultaneously: any number of |
462 multiple \emph{Query} windows may be active at the same time: any number of |
463 floating instances, but at most one docked instance (which is used by |
463 floating instances, but at most one docked instance (which is used by |
464 default). |
464 default). |
465 |
465 |
466 \begin{figure}[htb] |
466 \begin{figure}[htb] |
467 \begin{center} |
467 \begin{center} |