# HG changeset patch
# User wenzelm
# Date 1403119068 -7200
# Node ID 8b46b57008eac1c72d90f2ac42eab81c045d78ac
# Parent  e13c5dd9c7de2b0e743bd8be34edd63f14a48b49
misc tuning;

diff -r e13c5dd9c7de -r 8b46b57008ea src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Tue Jun 17 22:18:18 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Jun 18 21:17:48 2014 +0200
@@ -42,7 +42,7 @@
   \item [jEdit] is a sophisticated text editor implemented in
   Java.\footnote{@{url "http://www.jedit.org"}} It is easily extensible
   by plugins written in languages that work on the JVM, e.g.\
-  Scala\footnote{@{url "http://www.scala-lang.org/"}}.
+  Scala\footnote{@{url "http://www.scala-lang.org"}}.
 
   \item [Isabelle/jEdit] is the main example application of the PIDE
   framework and the default user-interface for Isabelle. It targets
@@ -71,49 +71,39 @@
   \label{fig:isabelle-jedit}
   \end{figure}
 
-  Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some
-  plugins for the well-known jEdit text editor
-  @{url "http://www.jedit.org"}, according to the following principles.
-
-  \begin{itemize}
-
-  \item The original jEdit look-and-feel is generally preserved,
-  although some default properties are changed to accommodate Isabelle
-  (e.g.\ the text area font).
+  Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for
+  the jEdit text editor, while preserving its general look-and-feel as far as
+  possible. The main plugin is called ``Isabelle'' and has its own menu
+  \emph{Plugins~/ Isabelle} with several panels (see also
+  \secref{sec:dockables}), as well as \emph{Plugins~/ Plugin Options~/
+  Isabelle} (see also \secref{sec:options}).
 
-  \item Formal Isabelle/Isar text is checked asynchronously while
-  editing.  The user is in full command of the editor, and the prover
-  refrains from locking portions of the buffer.
-
-  \item Prover feedback works via colors, boxes, squiggly underline,
-  hyperlinks, popup windows, icons, clickable output --- all based on
-  semantic markup produced by the prover process in the background.
-
-  \item Using the mouse together with the modifier key @{verbatim
-  CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
-  additional formal content via tooltips and/or hyperlinks.
+  The options allow to specify a logic session name --- the same selector is
+  accessible in the \emph{Theories} panel (\secref{sec:theories}). On
+  application startup, the selected logic session image is provided
+  automatically by the Isabelle build tool \cite{isabelle-sys}: if it is
+  absent or outdated wrt.\ its sources, the build process updates it before
+  entering the Prover IDE.  Changing the logic session within Isabelle/jEdit
+  requires a restart of the application.
 
-  \item Formal output (in popups etc.) may be explored recursively,
-  using the same techniques as in the editor source buffer.
-
-  \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
-  organized by the Dockable Window Manager of jEdit, which also allows
-  multiple floating instances of each window class.
-
-  \item The prover process and source files are managed on the editor
-  side.  The prover operates on timeless and stateless document
-  content as provided via Isabelle/Scala.
+  \medskip The main job of the Prover IDE is to manage sources and their
+  changes, taking the logical structure as a formal document into account (see
+  also \secref{sec:document-model}). The editor and the prover are connected
+  asynchronously in a lock-free manner. The prover is free to organize the
+  checking of the formal text in parallel on multiple cores, and provides
+  feedback via markup, which is rendered in the editor via colors, boxes,
+  squiggly underline, hyperlinks, popup windows, icons, clickable output etc.
 
-  \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give
-  access to a selection of Isabelle/Scala options and its persistent
-  preferences, usually with immediate effect on the prover back-end or
-  editor front-end.
+  Using the mouse together with the modifier key @{verbatim CONTROL} (Linux,
+  Windows) or @{verbatim COMMAND} (Mac OS X) exposes additional formal content
+  via tooltips and/or hyperlinks (see also \secref{sec:tooltips-hyperlinks}).
+  Formal output (in popups etc.) may be explored recursively, using the same
+  techniques as in the editor source buffer.
 
-  \item The logic image of the prover session may be specified within
-  Isabelle/jEdit.  The new image is provided automatically by the
-  Isabelle build tool after restart of the application.
-
-  \end{itemize}
+  Thus the Prover IDE gives an impression of direct access to formal content
+  of the prover within the editor, but in reality only certain aspects are
+  exposed, according to the possibilities of the prover and its many add-on
+  tools.
 *}
 
 
@@ -165,7 +155,7 @@
   Isabelle/jEdit. *}
 
 
-subsection {* Options *}
+subsection {* Options \label{sec:options} *}
 
 text {* Both jEdit and Isabelle have distinctive management of
   persistent options.
@@ -320,7 +310,7 @@
   take full effect.  *}
 
 
-section {* Dockable windows *}
+section {* Dockable windows \label{sec:dockables} *}
 
 text {*
   In jEdit terminology, a \emph{view} is an editor window with one or more
@@ -639,9 +629,9 @@
 *}
 
 
-chapter {* Prover IDE functionality *}
+chapter {* Prover IDE functionality \label{sec:document-model} *}
 
-section {* Document model *}
+section {* Document model \label{sec:document-model} *}
 
 text {*
   The document model is central to the PIDE architecture: the editor and the