more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
authorwenzelm
Sat, 20 Jul 2019 11:17:54 +0200
changeset 70382 23ba5a638e6d
parent 70381 b151d1f00204
child 70383 38ac2e714729
more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Jul 19 12:57:14 2019 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Jul 20 11:17:54 2019 +0200
@@ -148,7 +148,7 @@
 JEDIT_LOGIC_REQUIREMENTS=""
 JEDIT_LOGIC_FOCUS=""
 JEDIT_INCLUDE_SESSIONS=""
-JEDIT_SESSION_DIRS=""
+JEDIT_SESSION_DIRS="-"
 JEDIT_LOGIC=""
 JEDIT_PRINT_MODE=""
 JEDIT_NO_BUILD=""
@@ -182,11 +182,7 @@
         BUILD_ONLY=true
         ;;
       d)
-        if [ -z "$JEDIT_SESSION_DIRS" ]; then
-          JEDIT_SESSION_DIRS="$OPTARG"
-        else
-          JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
-        fi
+        JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
         ;;
       i)
         if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Jul 19 12:57:14 2019 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Sat Jul 20 11:17:54 2019 +0200
@@ -19,7 +19,7 @@
   /* session options */
 
   def session_dirs(): List[Path] =
-    Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+    Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-")
 
   def session_no_build(): Boolean =
     Isabelle_System.getenv("JEDIT_NO_BUILD") == "true"