# HG changeset patch # User wenzelm # Date 1612698941 -3600 # Node ID 4c8edf348c4e932ee44c0bb484fa62d6d5d6fee1 # Parent 3ab0cedaccadfa77381ec6a36e244de2a7e1f290 clarified modules: allow early invocation of Scala functions; diff -r 3ab0cedaccad -r 4c8edf348c4e src/Pure/PIDE/resources.ML --- 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>\scala_function\ + (Scan.lift Parse.embedded_position) check_scala_function #> + ML_Antiquotation.inline_embedded \<^binding>\scala_function\ + (Args.context -- Scan.lift Parse.embedded_position + >> (uncurry check_scala_function #> ML_Syntax.print_string)) #> + ML_Antiquotation.value_embedded \<^binding>\scala\ + (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>\scala_thread\ + (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 *) diff -r 3ab0cedaccad -r 4c8edf348c4e src/Pure/ROOT.ML --- 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"; diff -r 3ab0cedaccad -r 4c8edf348c4e src/Pure/System/scala.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>\scala_function\ - (Scan.lift Parse.embedded_position) check_function #> - ML_Antiquotation.inline_embedded \<^binding>\scala_function\ - (Args.context -- Scan.lift Parse.embedded_position - >> (uncurry check_function #> ML_Syntax.print_string)) #> - ML_Antiquotation.value_embedded \<^binding>\scala\ - (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>\scala_thread\ - (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;