# HG changeset patch
# User wenzelm
# Date 1655900328 -7200
# Node ID 99b7638d91774532a9d4e0bc527c1af1a193e287
# Parent  3bee51daf9a913c2c5fb9bdf22ddc71ecbee8d19
clarified session resources for bootstrap, notably for Scala functions;

diff -r 3bee51daf9a9 -r 99b7638d9177 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Wed Jun 22 14:16:45 2022 +0200
+++ b/src/Pure/ML/ml_process.scala	Wed Jun 22 14:18:48 2022 +0200
@@ -78,16 +78,14 @@
     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
 
     // session base
+    val (init_session_base, eval_init_session) =
+      session_base match {
+        case None => (sessions_structure.bootstrap, Nil)
+        case Some(base) => (base, List("Resources.init_session_env ()"))
+      }
     val init_session = Isabelle_System.tmp_file("init_session")
     Isabelle_System.chmod("600", File.path(init_session))
-    val eval_init_session =
-      session_base match {
-        case None => Nil
-        case Some(base) =>
-          File.write(init_session, new Resources(sessions_structure, base).init_session_yxml)
-          List("Resources.init_session_file (Path.explode " +
-            ML_Syntax.print_string_bytes(File.path(init_session).implode) + ")")
-      }
+    File.write(init_session, new Resources(sessions_structure, init_session_base).init_session_yxml)
 
     // process
     val eval_process =
@@ -119,9 +117,9 @@
 
     val bash_env = new HashMap(env)
     bash_env.put("ISABELLE_PROCESS_OPTIONS", File.standard_path(isabelle_process_options))
+    bash_env.put("ISABELLE_INIT_SESSION", File.standard_path(init_session))
     bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp))
     bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath)
-    bash_env.put("ISABELLE_SCALA_FUNCTIONS", Scala.functions.mkString(","))
 
     Bash.process(
       options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
diff -r 3bee51daf9a9 -r 99b7638d9177 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Jun 22 14:16:45 2022 +0200
+++ b/src/Pure/PIDE/resources.ML	Wed Jun 22 14:18:48 2022 +0200
@@ -17,14 +17,13 @@
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
   val init_session_yxml: string -> unit
-  val init_session_file: Path.T -> unit
+  val init_session_env: unit -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val check_session: Proof.context -> string * Position.T -> string
   val last_timing: Toplevel.transition -> Time.time
   val check_load_command: Proof.context -> string * Position.T -> string
-  val scala_functions: unit -> string list
   val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool)
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
@@ -152,8 +151,14 @@
        loaded_theories = loaded_theories}
   end;
 
-fun init_session_file path =
-  init_session_yxml (File.read path) before File.rm path;
+fun init_session_env () =
+  (case getenv "ISABELLE_INIT_SESSION" of
+    "" => ()
+  | name =>
+      try File.read (Path.explode name)
+      |> Option.app init_session_yxml);
+
+val _ = init_session_env ();
 
 fun finish_session_base () =
   Synchronized.change global_session_base
@@ -180,20 +185,12 @@
 
 (* Scala functions *)
 
-(*raw bootstrap environment*)
-fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
-
-val scala_function_default = the_default ((true, false), Position.none);
-
-(*regular resources*)
-fun scala_function a =
-  (a, scala_function_default (Symtab.lookup (get_session_base1 #scala_functions) a));
-
 fun check_scala_function ctxt arg =
   let
-    val funs = scala_functions () |> sort_strings |> map scala_function;
-    val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg;
-    val flags = #1 (scala_function_default (AList.lookup (op =) funs name));
+    val table = get_session_base1 #scala_functions;
+    val funs = Symtab.fold (fn (a, (_, pos)) => cons (a, pos)) table [] |> sort_by #1;
+    val name = Completion.check_entity Markup.scala_functionN funs ctxt arg;
+    val flags = #1 (the (Symtab.lookup table name));
   in (name, flags) end;
 
 val _ = Theory.setup