more systematic support for special directories;

--- a/NEWS	Mon Aug 17 12:35:03 2020 +0200
+++ b/NEWS	Mon Aug 17 13:16:42 2020 +0200
@@ -138,6 +138,12 @@
 
 *** System ***
 
+* The shell function "isabelle_directory" (within etc/settings of
+components) augments the list of special directories for persistent
+symbolic path names. This improves portability of heap images and
+session databases. It used to be hard-wired for Isabelle + AFP, but
+other projects may now participate on equal terms.
+
 * ML statistics via an external Poly/ML process: this allows monitoring
 the runtime system while the ML program sleeps.
 

--- a/etc/settings	Mon Aug 17 12:35:03 2020 +0200
+++ b/etc/settings	Mon Aug 17 13:16:42 2020 +0200
@@ -74,6 +74,10 @@
 ### Misc path settings
 ###
 
+isabelle_directory '~'
+isabelle_directory '$ISABELLE_HOME_USER'
+isabelle_directory '~~'
+
 ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"
 ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib"
 

--- a/lib/scripts/getfunctions	Mon Aug 17 12:35:03 2020 +0200
+++ b/lib/scripts/getfunctions	Mon Aug 17 13:16:42 2020 +0200
@@ -160,6 +160,22 @@
 }
 export -f isabelle_scala_service
 
+#Special directories
+function isabelle_directory ()
+{
+  local X=""
+  for X in "$@"
+  do
+    if [ -z "$ISABELLE_DIRECTORIES" ]; then
+      ISABELLE_DIRECTORIES="$X"
+    else
+      ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X"
+    fi
+  done
+  export ISABELLE_DIRECTORIES
+}
+export -f isabelle_directory
+
 #administrative build
 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   function isabelle_admin_build ()

--- a/lib/scripts/getsettings	Mon Aug 17 12:35:03 2020 +0200
+++ b/lib/scripts/getsettings	Mon Aug 17 13:16:42 2020 +0200
@@ -57,6 +57,7 @@
 ISABELLE_FONTS=""
 ISABELLE_FONTS_HIDDEN=""
 ISABELLE_SCALA_SERVICES=""
+ISABELLE_DIRECTORIES=""
 
 #main executables
 ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"

--- a/src/Pure/General/path.ML	Mon Aug 17 12:35:03 2020 +0200
+++ b/src/Pure/General/path.ML	Mon Aug 17 13:16:42 2020 +0200
@@ -36,7 +36,7 @@
   val exe: T -> T
   val expand: T -> T
   val file_name: T -> string
-  val smart_implode: T -> string
+  val implode_symbolic: T -> string
   val position: T -> Position.T
   eqtype binding
   val binding: T * Position.T -> binding
@@ -235,10 +235,11 @@
 val file_name = implode_path o base o expand;
 
 
-(* smart implode *)
+(* implode wrt. given directories *)
 
-fun smart_implode path =
+fun implode_symbolic path =
   let
+    val directories = rev (space_explode ":" (getenv "ISABELLE_DIRECTORIES"));
     val full_name = implode_path (expand path);
     fun fold_path a =
       (case try (implode_path o expand o explode_path) a of
@@ -250,12 +251,12 @@
             | NONE => NONE)
       | NONE => NONE);
   in
-    (case get_first fold_path ["$AFP", "~~", "$ISABELLE_HOME_USER", "~"] of
+    (case get_first fold_path directories of
       SOME name => name
     | NONE => implode_path path)
   end;
 
-val position = Position.file o smart_implode;
+val position = Position.file o implode_symbolic;
 
 
 (* binding: strictly monotonic path with position *)

--- a/src/Pure/PIDE/resources.ML	Mon Aug 17 12:35:03 2020 +0200
+++ b/src/Pure/PIDE/resources.ML	Mon Aug 17 13:16:42 2020 +0200
@@ -130,7 +130,7 @@
 
 fun begin_theory master_dir {name, imports, keywords} parents =
   Theory.begin_theory name parents
-  |> map_files (fn _ => (Path.explode (Path.smart_implode master_dir), imports, []))
+  |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, []))
   |> Thy_Header.add_keywords keywords;
 
 
@@ -259,7 +259,7 @@
       | NONE => master_directory (Proof_Context.theory_of ctxt));
     val path = Path.append dir (Path.explode name) handle ERROR msg => err msg;
     val _ = Path.expand path handle ERROR msg => err msg;
-    val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
+    val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
     val _ = check_file path handle ERROR msg => err msg;
   in path end;
 

--- a/src/Tools/Code/code_target.ML	Mon Aug 17 12:35:03 2020 +0200
+++ b/src/Tools/Code/code_target.ML	Mon Aug 17 13:16:42 2020 +0200
@@ -536,7 +536,7 @@
             Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos);
       val _ = Position.report pos Markup.language_path;
       val path = #1 (Path.explode_pos (s, pos));
-      val _ = Position.report pos (Markup.path (Path.smart_implode path));
+      val _ = Position.report pos (Markup.path (Path.implode_symbolic path));
     in (location, (path, pos)) end;
 
 fun export_code all_public cs seris lthy =