diff -r b0cdb4b10d20 -r 5cbe32533cdb src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Tue Oct 29 21:00:37 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Wed Oct 30 17:05:23 2013 +0100
@@ -245,9 +245,58 @@
   order to take full effect.  *}
 
 
+subsection {* File-system access *}
+
+text {* File specifications in jEdit follow various formats and
+  conventions according to \emph{Virtual File Systems}, which may be
+  also provided by additional plugins.  This allows to access remote
+  files via the @{verbatim "http:"} protocol prefix, for example.
+  Isabelle/jEdit attempts to work with the file-system access model of
+  jEdit as far as possible.  In particular, theory sources are passed
+  directly from the editor to the prover, without indirection via
+  files.
+
+  Despite the flexibility of URLs in jEdit, local files are
+  particularly important and are accessible without protocol prefix.
+  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 Unix/POSIX forward slashes, 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 on Windows uses Cygwin
+  file-system access.}  Moreover, environment variables from the
+  Isabelle process may be used freely, e.g.\ @{file
+  "$ISABELLE_HOME/etc/symbols"} or @{file
+  "$ISABELLE_JDK_HOME/README.html"}.  There are special shortcuts:
+  @{verbatim "~"} for @{file "$USER_HOME"}, and @{verbatim "~~"} 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 at least @{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.
+
+  Moreover note that path specifications in prover input or output
+  usually include formal markup that turns it into a hyperlink (see
+  also \secref{sec:theory-source}).  This allows to open the
+  corresponding file in the text editor, independently of the path
+  notation.  *}
+
+
 chapter {* Prover IDE functionality *}
 
-section {* Text buffers and theories *}
+section {* Text buffers and theories \label{sec:theory-source} *}
 
 text {* As regular text editor, jEdit maintains a collection of open
   \emph{text buffers} to store source files; each buffer may be