# HG changeset patch
# User wenzelm
# Date 1472736548 -7200
# Node ID 4fe8cfaeb1fcd83f3be3f9fe5ab16c02cc434f2a
# Parent  ebcc70c120a9f3609f6f77c29fa9a5043612bfb9
clarified important directories;

diff -r ebcc70c120a9 -r 4fe8cfaeb1fc src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Sep 01 15:18:14 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Thu Sep 01 15:29:08 2016 +0200
@@ -166,8 +166,7 @@
   Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global
   Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
   two within the central options dialog. Changes are stored in @{path
-  "$ISABELLE_HOME_USER/jedit/properties"} and @{path
-  "$ISABELLE_HOME_USER/jedit/keymaps"}.
+  "$JEDIT_SETTINGS/properties"} and @{path "$JEDIT_SETTINGS/keymaps"}.
 
   Isabelle system options are managed by Isabelle/Scala and changes are stored
   in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of
@@ -193,7 +192,7 @@
   \<^medskip>
   Options are usually loaded on startup and saved on shutdown of
   Isabelle/jEdit. Editing the machine-generated @{path
-  "$ISABELLE_HOME_USER/jedit/properties"} or @{path
+  "$JEDIT_SETTINGS/properties"} or @{path
   "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
   running is likely to cause surprise due to lost update!
 \<close>
@@ -212,8 +211,8 @@
   Isabelle/jEdit due to various fine-tuning of global defaults, with
   additional keyboard shortcuts for Isabelle-specific functionality. Users may
   change their keymap later, but need to copy some keyboard shortcuts manually
-  (see also @{path "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close>
-  properties in \<^file>\<open>$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props\<close>).
+  (see also @{path "$JEDIT_SETTINGS/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties in
+  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>).
 \<close>
 
 
@@ -671,10 +670,11 @@
   wrapper, in contrast to @{tool jedit} run from the command line
   (\secref{sec:command-line}).
 
-  Isabelle/jEdit imitates \<^verbatim>\<open>$ISABELLE_HOME\<close> and \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> 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>\<open>Favorites\<close> for these two important locations.
+  Isabelle/jEdit imitates important system settings within the Java process
+  environment, in order to allow easy access to these important places from
+  the editor: \<^verbatim>\<open>$ISABELLE_HOME\<close>, \<^verbatim>\<open>$ISABELLE_HOME_USER\<close>, \<^verbatim>\<open>$JEDIT_HOME\<close>,
+  \<^verbatim>\<open>$JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<open>Favorites\<close> for
+  these two important locations.
 
   \<^medskip>
   Path specifications in prover input or output usually include formal markup
diff -r ebcc70c120a9 -r 4fe8cfaeb1fc src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Thu Sep 01 15:18:14 2016 +0200
+++ b/src/Pure/Tools/main.scala	Thu Sep 01 15:29:08 2016 +0200
@@ -100,11 +100,15 @@
     {
       val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
       val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER")
+      val jedit_home = Isabelle_System.getenv("JEDIT_HOME")
+      val jedit_settings = Isabelle_System.getenv("JEDIT_SETTINGS")
 
       (env0: Any) => {
         val env = env0.asInstanceOf[java.util.Map[String, String]]
         env.put("ISABELLE_HOME", File.platform_path(isabelle_home))
         env.put("ISABELLE_HOME_USER", File.platform_path(isabelle_home_user))
+        env.put("JEDIT_HOME", File.platform_path(jedit_home))
+        env.put("JEDIT_SETTINGS", File.platform_path(jedit_settings))
         env.remove("ISABELLE_ROOT")
       }
     }
diff -r ebcc70c120a9 -r 4fe8cfaeb1fc src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Thu Sep 01 15:18:14 2016 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Thu Sep 01 15:29:08 2016 +0200
@@ -281,6 +281,10 @@
 vfs.favorite.0=$ISABELLE_HOME
 vfs.favorite.1.type=1
 vfs.favorite.1=$ISABELLE_HOME_USER
+vfs.favorite.2.type=1
+vfs.favorite.2=$JEDIT_HOME
+vfs.favorite.3.type=1
+vfs.favorite.3=$JEDIT_SETTINGS
 view.antiAlias=standard
 view.blockCaret=true
 view.caretBlink=false