# HG changeset patch
# User wenzelm
# Date 1563614274 -7200
# Node ID 23ba5a638e6d850b27e67e3e89cb06a59932e74a
# Parent  b151d1f00204e6e6fed7a6fe5b122484b1c6cfa1
more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;

diff -r b151d1f00204 -r 23ba5a638e6d src/Tools/jEdit/lib/Tools/jedit
--- 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
diff -r b151d1f00204 -r 23ba5a638e6d src/Tools/jEdit/src/jedit_sessions.scala
--- 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"