more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
--- 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"