1.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Oct 31 16:10:35 2013 +0100
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Oct 31 16:47:36 2013 +0100
     1.3 @@ -407,7 +407,7 @@
     1.4  
     1.5    The main purpose of the output window is to ``debug'' unclear
     1.6    situations by inspecting internal state of the prover.\footnote{In
     1.7 -  that sense, unstructured tactic scripts depend on continous
     1.8 +  that sense, unstructured tactic scripts depend on continuous
     1.9    debugging with internal state inspection.} Consequently, some
    1.10    special messages for \emph{tracing} or \emph{proof state} only
    1.11    appear here, and are not attached to the original source.
    1.12 @@ -415,7 +415,8 @@
    1.13    \medskip In any case, prover messages also contain markup that may
    1.14    be explored recursively via tooltips or hyperlinks (see
    1.15    \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate
    1.16 -  certain actions (e.g.\ see \secref{sec:sledgehammer}).  *}
    1.17 +  certain actions (see \secref{sec:auto-tools} and
    1.18 +  \secref{sec:sledgehammer}).  *}
    1.19  
    1.20  
    1.21  section {* Tooltips and hyperlinks \label{sec:tooltips-hyperlinks} *}
    1.22 @@ -663,7 +664,7 @@
    1.23  *}
    1.24  
    1.25  
    1.26 -section {* Automatically tried tools *}
    1.27 +section {* Automatically tried tools \label{sec:auto-tools} *}
    1.28  
    1.29  text {* Continuous document processing works asynchronously in the
    1.30    background.  Visible document source that has been evaluated already
    1.31 @@ -761,16 +762,39 @@
    1.32  
    1.33  section {* Sledgehammer \label{sec:sledgehammer} *}
    1.34  
    1.35 -text {*
    1.36 -  FIXME
    1.37 -*}
    1.38 +text {* The \emph{Sledgehammer} panel provides a view on some
    1.39 +  independent execution of @{command sledgehammer}, with process
    1.40 +  indicator (spinning wheel) and GUI elements for important
    1.41 +  Sledgehammer arguments and options.  Any number of Sledgehammer
    1.42 +  panels may be active, according to the standard policies of Dockable
    1.43 +  Window Management in jEdit.  Closing a window also cancels the
    1.44 +  corresponding prover tasks.
    1.45 +
    1.46 +  The \emph{Apply} button attaches a fresh invocation of @{command
    1.47 +  sledgehammer} to the command where the cursor is pointing in the
    1.48 +  text --- this should be some pending proof problem.  Further buttons
    1.49 +  like \emph{Cancel} and \emph{Locate} help to manage the running
    1.50 +  process.
    1.51 +
    1.52 +  Results appear incrementally in the output window of the panel.
    1.53 +  Proposed proof snippets are marked up as \emph{sendback}, which
    1.54 +  means a single mouse click inserts the text into a suitable place of
    1.55 +  the original source.  Some manual editing may be required
    1.56 +  nonetheless, say to remove earlier proof attempts. *}
    1.57  
    1.58  
    1.59  section {* Find theorems *}
    1.60  
    1.61 -text {*
    1.62 -  FIXME
    1.63 -*}
    1.64 +text {* The \emph{Find} panel provides an independent view for
    1.65 +  @{command find_theorems}.  The main text field accepts search
    1.66 +  criteria according to the syntax @{syntax thmcriterium} given in
    1.67 +  \cite{isabelle-isar-ref}.  Further options of @{command
    1.68 +  find_theorems} are available via GUI elements.
    1.69 +
    1.70 +  The \emph{Apply} button attaches a fresh invocation of @{command
    1.71 +  find_theorems} to the current context of the command where the
    1.72 +  cursor is pointing in the text, unless an alternative theory context
    1.73 +  (from the underlying logic image) is specified explicitly. *}
    1.74  
    1.75  
    1.76  chapter {* Known problems and workarounds \label{sec:problems} *}