src/Doc/JEdit/JEdit.thy

   Here the path notation is that of the Java Virtual Machine on the
   underlying platform.  On Windows the preferred form uses
   backslashes, but happens to accept forward slashes of Unix/POSIX, too.
   Further differences arise due to drive letters and network shares.
 
-  The Java notation for files needs to be distinguished from the one
-  of Isabelle, which uses POSIX notation with forward slashes on
-  \emph{all} platforms.\footnote{Isabelle/ML on Windows uses Cygwin
-  file-system access.}  Moreover, environment variables from the
+  The Java notation for files needs to be distinguished from the one of
+  Isabelle, which uses POSIX notation with forward slashes on \emph{all}
+  platforms.\footnote{Isabelle/ML on Windows uses Cygwin file-system access
+  and Unix-style path notation.} Moreover, environment variables from the
   Isabelle process may be used freely, e.g.\ @{file
   "$ISABELLE_HOME/etc/symbols"} or @{file_unchecked "$POLYML_HOME/README"}.
-  There are special shortcuts: @{file "~"} for @{file "$USER_HOME"}
-  and @{file "~~"} for @{file "$ISABELLE_HOME"}.
+  There are special shortcuts: @{file "~"} for @{file "$USER_HOME"} and @{file
+  "~~"} for @{file "$ISABELLE_HOME"}.
 
   \medskip Since jEdit happens to support environment variables within
   file specifications as well, it is natural to use similar notation
   within the editor, e.g.\ in the file-browser.  This does not work in
   full generality, though, due to the bias of jEdit towards
   platform-specific notation and of Isabelle towards POSIX.  Moreover,
   the Isabelle settings environment is not yet active when starting
   Isabelle/jEdit via its standard application wrapper (in contrast to
   @{verbatim "isabelle jedit"} run from the command line).
 
-  For convenience, Isabelle/jEdit imitates @{verbatim "$ISABELLE_HOME"} and
-  @{verbatim "$ISABELLE_HOME_USER"} within the Java process environment, in
-  order to allow easy access to these important places from the editor. The
-  file browser of jEdit also includes \emph{Favorites} for these two important
+  Isabelle/jEdit imitates @{verbatim "$ISABELLE_HOME"} and @{verbatim
+  "$ISABELLE_HOME_USER"} within the Java process environment, in order to
+  allow easy access to these important places from the editor. The file
+  browser of jEdit also includes \emph{Favorites} for these two important
   locations.
 
   \medskip Path specifications in prover input or output usually include
   formal markup that turns it into a hyperlink (see also
   \secref{sec:tooltips-hyperlinks}). This allows to open the corresponding

   Otherwise the corresponding key event retains its standard meaning
   within the underlying text area.
 *}
 
 
-subsection {* Rendering *}
-
-text {*
-  FIXME
-*}
-
-
 subsection {* Insertion \label{sec:completion-insert} *}
 
 text {*
   FIXME