--- a/NEWS Tue Oct 29 21:00:37 2013 +0100
+++ b/NEWS Wed Oct 30 17:05:23 2013 +0100
@@ -102,8 +102,8 @@
(cf. keyboard shortcut C+0).
* File specifications in jEdit (e.g. file browser) may refer to
-$ISABELLE_HOME on all platforms. Discontinued obsolete
-$ISABELLE_HOME_WINDOWS variable.
+$ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms. Discontinued
+obsolete $ISABELLE_HOME_WINDOWS variable.
* Improved support for Linux look-and-feel "GTK+", see also "Utilities
/ Global Options / Appearance".
--- 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
--- a/src/Pure/Tools/main.scala Tue Oct 29 21:00:37 2013 +0100
+++ b/src/Pure/Tools/main.scala Wed Oct 30 17:05:23 2013 +0100
@@ -225,11 +225,17 @@
val update =
{
val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
+ val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER")
val upd =
if (Platform.is_windows)
- List("ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home), "INI_DIR" -> "")
+ List(
+ "ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home),
+ "ISABELLE_HOME_USER" -> Isabelle_System.jvm_path(isabelle_home_user),
+ "INI_DIR" -> "")
else
- List("ISABELLE_HOME" -> isabelle_home)
+ List(
+ "ISABELLE_HOME" -> isabelle_home,
+ "ISABELLE_HOME_USER" -> isabelle_home_user)
(env0: Any) => {
val env = env0.asInstanceOf[java.util.Map[String, String]]