# HG changeset patch # User wenzelm # Date 1590342342 -7200 # Node ID 71de0a25384246efb9a05927f077c4723ffa8d5b # Parent 0ca3535217530c90b498c61488b1342a2209dea7 proper check of registered Scala functions; diff -r 0ca353521753 -r 71de0a253842 etc/symbols --- 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 diff -r 0ca353521753 -r 71de0a253842 lib/texinputs/isabellesym.sty --- 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}} diff -r 0ca353521753 -r 71de0a253842 src/Pure/ML/ml_process.scala --- 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 = () => { diff -r 0ca353521753 -r 71de0a253842 src/Pure/PIDE/markup.ML --- 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 *) diff -r 0ca353521753 -r 71de0a253842 src/Pure/ROOT.ML --- 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"; diff -r 0ca353521753 -r 71de0a253842 src/Pure/System/scala.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>\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))); end; diff -r 0ca353521753 -r 71de0a253842 src/Pure/System/scala.scala --- 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 diff -r 0ca353521753 -r 71de0a253842 src/Pure/System/scala_check.ML --- /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>\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; + +end; diff -r 0ca353521753 -r 71de0a253842 src/Pure/Thy/bibtex.ML --- 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>\check_bibtex_database\ 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));