proper check of registered Scala functions;

--- a/etc/symbols	Sun May 24 14:47:28 2020 +0200
+++ b/etc/symbols	Sun May 24 19:45:42 2020 +0200
@@ -417,6 +417,8 @@
 \<^plugin>              argument: cartouche
 \<^print>
 \<^prop>                argument: cartouche
+\<^scala>               argument: cartouche
+\<^scala_function>      argument: cartouche
 \<^session>             argument: cartouche
 \<^simproc>             argument: cartouche
 \<^sort>                argument: cartouche

--- a/lib/texinputs/isabellesym.sty	Sun May 24 14:47:28 2020 +0200
+++ b/lib/texinputs/isabellesym.sty	Sun May 24 19:45:42 2020 +0200
@@ -402,6 +402,8 @@
 \newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
 \newcommand{\isactrlprint}{\isakeywordcontrol{print}}
 \newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
+\newcommand{\isactrlscala}{\isakeywordcontrol{scala}}
+\newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}}
 \newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
 \newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
 \newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}

--- a/src/Pure/ML/ml_process.scala	Sun May 24 14:47:28 2020 +0200
+++ b/src/Pure/ML/ml_process.scala	Sun May 24 19:45:42 2020 +0200
@@ -113,6 +113,8 @@
     val isabelle_tmp = Isabelle_System.tmp_dir("process")
     val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
 
+    val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(","))
+
     val ml_runtime_options =
     {
       val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
@@ -135,7 +137,7 @@
       "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
         Bash.strings(bash_args),
       cwd = cwd,
-      env = env ++ env_options ++ env_tmp,
+      env = env ++ env_options ++ env_tmp ++ env_functions,
       redirect = redirect,
       cleanup = () =>
         {

--- a/src/Pure/PIDE/markup.ML	Sun May 24 14:47:28 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun May 24 19:45:42 2020 +0200
@@ -68,6 +68,7 @@
   val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
+  val scala_functionN: string val scala_function: string -> T
   val markupN: string
   val consistentN: string
   val unbreakableN: string
@@ -405,6 +406,7 @@
 val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
+val (scala_functionN, scala_function) = markup_string "scala_function" nameN;
 
 
 (* pretty printing *)

--- a/src/Pure/ROOT.ML	Sun May 24 14:47:28 2020 +0200
+++ b/src/Pure/ROOT.ML	Sun May 24 19:45:42 2020 +0200
@@ -328,6 +328,7 @@
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
 ML_file "System/scala.ML";
+ML_file "System/scala_check.ML";
 ML_file "Thy/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";

--- a/src/Pure/System/scala.ML	Sun May 24 14:47:28 2020 +0200
+++ b/src/Pure/System/scala.ML	Sun May 24 19:45:42 2020 +0200
@@ -6,10 +6,11 @@
 
 signature SCALA =
 sig
+  val functions: unit -> string list
+  val check_function: Proof.context -> string * Position.T -> string
   val promise_function: string -> string -> string future
   val function: string -> string -> string
   exception Null
-  val check: string -> unit
 end;
 
 structure Scala: SCALA =
@@ -70,14 +71,37 @@
         handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
 
 
+(* registered functions *)
 
-(** check source snippet **)
+fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
 
-fun check source =
-  let val errors =
-    function "scala_check" source
-    |> YXML.parse_body
-    |> let open XML.Decode in list string end
-  in if null errors then () else error (cat_lines errors) end;
+fun check_function ctxt (name, pos) =
+  let
+    val kind = Markup.scala_functionN;
+    val funs = functions ();
+  in
+    if member (op =) funs name then
+      (Context_Position.report ctxt pos (Markup.scala_function name); name)
+    else
+      let
+        val completion_report =
+          Completion.make_report (name, pos)
+            (fn completed =>
+              filter completed funs
+              |> sort_strings
+              |> map (fn a => (a, (kind, a))));
+      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end
+  end;
+
+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)));
 
 end;

--- a/src/Pure/System/scala.scala	Sun May 24 14:47:28 2020 +0200
+++ b/src/Pure/System/scala.scala	Sun May 24 19:45:42 2020 +0200
@@ -99,6 +99,9 @@
   /* registered functions */
 
   sealed case class Fun(name: String, apply: String => String)
+  {
+    override def toString: String = name
+  }
 
   lazy val functions: List[Fun] =
     Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/scala_check.ML	Sun May 24 19:45:42 2020 +0200
@@ -0,0 +1,22 @@
+(*  Title:      Pure/System/scala_check.ML
+    Author:     Makarius
+
+Semantic check of Scala sources.
+*)
+
+signature SCALA_CHECK =
+sig
+  val decl: string -> unit
+end;
+
+structure Scala_Check: SCALA_CHECK =
+struct
+
+fun decl source =
+  let val errors =
+    \<^scala>\<open>scala_check\<close> source
+    |> YXML.parse_body
+    |> let open XML.Decode in list string end
+  in if null errors then () else error (cat_lines errors) end;
+
+end;

--- a/src/Pure/Thy/bibtex.ML	Sun May 24 14:47:28 2020 +0200
+++ b/src/Pure/Thy/bibtex.ML	Sun May 24 19:45:42 2020 +0200
@@ -20,7 +20,7 @@
 type message = string * Position.T;
 
 fun check_database pos0 database =
-  Scala.function "check_bibtex_database" database
+  \<^scala>\<open>check_bibtex_database\<close> database
   |> YXML.parse_body
   |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
   |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));