clarified modules: allow early invocation of Scala functions;

--- a/src/Pure/PIDE/resources.ML	Sun Feb 07 12:30:52 2021 +0100
+++ b/src/Pure/PIDE/resources.ML	Sun Feb 07 12:55:41 2021 +0100
@@ -24,7 +24,8 @@
   val check_session: Proof.context -> string * Position.T -> string
   val session_chapter: string -> string
   val last_timing: Toplevel.transition -> Time.time
-  val scala_function_pos: string -> Position.T
+  val scala_functions: unit -> string list
+  val check_scala_function: Proof.context -> string * Position.T -> string
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -175,9 +176,34 @@
 
 fun last_timing tr = get_timings (get_session_base1 #timings) tr;
 
+
+(* Scala functions *)
+
+(*raw bootstrap environment*)
+fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
+
+(*regular resources*)
 fun scala_function_pos name =
-  Symtab.lookup (get_session_base1 #scala_functions) name
-  |> the_default Position.none;
+  (name, the_default Position.none (Symtab.lookup (get_session_base1 #scala_functions) name));
+
+fun check_scala_function ctxt arg =
+  Completion.check_entity Markup.scala_functionN
+    (scala_functions () |> sort_strings |> map scala_function_pos) ctxt arg;
+
+val _ = Theory.setup
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
+    (Scan.lift Parse.embedded_position) check_scala_function #>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
+    (Args.context -- Scan.lift Parse.embedded_position
+      >> (uncurry check_scala_function #> ML_Syntax.print_string)) #>
+  ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
+    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+      let val name = check_scala_function ctxt arg
+      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #>
+  ML_Antiquotation.value_embedded \<^binding>\<open>scala_thread\<close>
+    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+      let val name = check_scala_function ctxt arg
+      in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end)));
 
 
 (* manage source files *)

--- a/src/Pure/ROOT.ML	Sun Feb 07 12:30:52 2021 +0100
+++ b/src/Pure/ROOT.ML	Sun Feb 07 12:55:41 2021 +0100
@@ -293,6 +293,7 @@
 
 (*Isabelle system*)
 ML_file "PIDE/protocol_command.ML";
+ML_file "System/scala.ML";
 ML_file "System/bash.ML";
 ML_file "System/isabelle_system.ML";
 
@@ -325,7 +326,6 @@
 ML_file "System/command_line.ML";
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
-ML_file "System/scala.ML";
 ML_file "System/scala_compiler.ML";
 ML_file "System/isabelle_tool.ML";
 ML_file "Thy/bibtex.ML";

--- a/src/Pure/System/scala.ML	Sun Feb 07 12:30:52 2021 +0100
+++ b/src/Pure/System/scala.ML	Sun Feb 07 12:55:41 2021 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/System/scala.ML
     Author:     Makarius
 
-Support for Scala at runtime.
+Invoke Scala functions from the ML runtime.
 *)
 
 signature SCALA =
@@ -9,15 +9,11 @@
   exception Null
   val function: string -> string -> string
   val function_thread: string -> string -> string
-  val functions: unit -> string list
-  val check_function: Proof.context -> string * Position.T -> string
 end;
 
 structure Scala: SCALA =
 struct
 
-(** protocol for Scala function invocation from ML **)
-
 exception Null;
 
 local
@@ -71,29 +67,4 @@
 
 end;
 
-
-
-(** registered Scala functions **)
-
-fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
-
-fun check_function ctxt arg =
-  Completion.check_entity Markup.scala_functionN
-    (functions () |> sort_strings |> map (fn a => (a, Resources.scala_function_pos a))) ctxt arg;
-
-val _ = Theory.setup
- (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
-   (Scan.lift Parse.embedded_position) check_function #>
-  ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
-    (Args.context -- Scan.lift Parse.embedded_position
-      >> (uncurry check_function #> ML_Syntax.print_string)) #>
-  ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
-    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
-      let val name = check_function ctxt arg
-      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #>
-  ML_Antiquotation.value_embedded \<^binding>\<open>scala_thread\<close>
-    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
-      let val name = check_function ctxt arg
-      in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end)));
-
 end;