--- 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 {*