# HG changeset patch
# User wenzelm
# Date 1402916791 -7200
# Node ID 1a3daaaa25c2c7b04d2382bd725d5fc666b0d7e0
# Parent  d8a64a4cbfca89c61a46fb966b17e55d40c2cac0
tuned;

diff -r d8a64a4cbfca -r 1a3daaaa25c2 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Jun 16 12:52:20 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Mon Jun 16 13:06:31 2014 +0200
@@ -595,14 +595,14 @@
   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
@@ -613,10 +613,10 @@
   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
@@ -1323,13 +1323,6 @@
 *}
 
 
-subsection {* Rendering *}
-
-text {*
-  FIXME
-*}
-
-
 subsection {* Insertion \label{sec:completion-insert} *}
 
 text {*