src/Doc/JEdit/JEdit.thy

 section \<open>Automatically tried tools \label{sec:auto-tools}\<close>
 
 text \<open>
   Continuous document processing works asynchronously in the background.
   Visible document source that has been evaluated may get augmented by
-  additional results of \<^emph>\<open>asynchronous print functions\<close>. The canonical example
-  is proof state output, which is always enabled. More heavy-weight print
-  functions may be applied, in order to prove or disprove parts of the formal
-  text by other means.
+  additional results of \<^emph>\<open>asynchronous print functions\<close>. An example for that
+  is proof state output, if that is enabled in the Output panel
+  (\secref{sec:output}). More heavy-weight print functions may be applied as
+  well, e.g.\ to prove or disprove parts of the formal text by other means.
 
   Isabelle/HOL provides various automatically tried tools that operate on
   outermost goal statements (e.g.\ @{command lemma}, @{command theorem}),
   independently of the state of the current proof attempt. They work
   implicitly without any arguments. Results are output as \<^emph>\<open>information
   messages\<close>, which are indicated in the text area by blue squiggles and a blue
   information sign in the gutter (see \figref{fig:auto-tools}). The message
   content may be shown as for other output (see also \secref{sec:output}).
   Some tools produce output with \<^emph>\<open>sendback\<close> markup, which means that clicking
-  on certain parts of the output inserts that text into the source in the
-  proper place.
+  on certain parts of the text inserts that into the source in the proper
+  place.
 
   \begin{figure}[!htb]
   \begin{center}
   \includegraphics[scale=0.333]{auto-tools}
   \end{center}

 
 
 section \<open>Markdown structure\<close>
 
 text \<open>
-  FIXME
-  \figref{fig:markdown-document}
+  Document text is internally structured in paragraphs and nested lists, using
+  notation that is similar to Markdown\<^footnote>\<open>@{url "http://commonmark.org"}\<close>. There
+  are special control symbols for items of different kinds of lists,
+  corresponding to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This
+  is illustrated in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
 
   \begin{figure}[!htb]
   \begin{center}
   \includegraphics[scale=0.333]{markdown-document}
   \end{center}
   \caption{Markdown structure within document text}
   \label{fig:markdown-document}
   \end{figure}
+
+  Items take colour according to the depth of nested lists. This helps to
+  explore the implicit rules for list structure interactively. There is also
+  markup for individual paragraphs in the text: it may be explored via mouse
+  hovering with \<^verbatim>\<open>CONTROL\<close> / \<^verbatim>\<open>COMMAND\<close> as usual
+  (\secref{sec:tooltips-hyperlinks}).
 \<close>
 
 
 section \<open>Citations and Bib{\TeX} entries \label{sec:bibtex}\<close>
 

   individual command timings are shown as well. A double-click on a theory
   node or command moves the editor focus to that particular source position.
 
   It is also possible to reveal individual timing information via some tooltip
   for the corresponding command keyword, using the technique of mouse hovering
-  with \<^verbatim>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> modifier key as explained in
-  \secref{sec:tooltips-hyperlinks}. Actual display of timing depends on the
-  global option @{system_option_ref jedit_timing_threshold}, which can be
-  configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>.
+  with \<^verbatim>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> modifier (\secref{sec:tooltips-hyperlinks}).
+  Actual display of timing depends on the global option @{system_option_ref
+  jedit_timing_threshold}, which can be configured in \<^emph>\<open>Plugin Options~/
+  Isabelle~/ General\<close>.
 
   \<^medskip>
   The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent
   activity of the Isabelle/ML task farm and the underlying ML runtime system.
   The display is continuously updated according to @{system_option_ref

 
 
 section \<open>Low-level output\<close>
 
 text \<open>
-  Prover output is normally shown directly in the main text area or secondary
-  \<^emph>\<open>Output\<close> panels, as explained in \secref{sec:output}.
-
-  Beyond this, it is occasionally useful to inspect low-level output channels
-  via some of the following additional panels:
+  Prover output is normally shown directly in the main text area or specific
+  panels like \<^emph>\<open>Output\<close> (\secref{sec:output}) or \<^emph>\<open>State\<close>
+  (\secref{sec:state-output}). Beyond this, it is occasionally useful to
+  inspect low-level output channels via some of the following additional
+  panels:
 
   \<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the Isabelle/Scala and
   Isabelle/ML side of the PIDE document editing protocol. Recording of
   messages starts with the first activation of the corresponding dockable
   window; earlier messages are lost.