# HG changeset patch
# User wenzelm
# Date 1402083770 -7200
# Node ID 742688bc1b16221263d9e1637f69c7da740c0785
# Parent  c66832858f433747dd65d1034ffa48623d215cf1
tuned;

diff -r c66832858f43 -r 742688bc1b16 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri Jun 06 21:35:23 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Fri Jun 06 21:42:50 2014 +0200
@@ -451,15 +451,15 @@
 
 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.
+  information from the prover In old times the user would have issued some
+  diagnostic command like @{command find_theorems} and inspected its output,
+  but this is now integrated 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}, see also \figref{fig:query}. As usual in jEdit,
-  multiple \emph{Query} windows may be active simultaneously: any number of
+  \emph{Print Context}, e.g.\ see \figref{fig:query}. As usual in jEdit,
+  multiple \emph{Query} windows may be active at the same time: any number of
   floating instances, but at most one docked instance (which is used by
   default).
 
@@ -471,7 +471,7 @@
   \label{fig:query}
   \end{figure}
 
-  \medskip The following GUI elements are common to all modes of query:
+  \medskip The following GUI elements are common to all query modes:
   \begin{itemize}
 
   \item The spinning wheel provides feedback about the status of a pending