# HG changeset patch
# User wenzelm
# Date 1590347483 -7200
# Node ID 45f85e283ce075981e52f02f612dbcd796e96d27
# Parent  86cfb9fa3da82b14c3bcb5e2a247ae422b9d01d6# Parent  2bf0283fc9755a9d6b8e868f116c4ae0574f5c64
merged

diff -r 86cfb9fa3da8 -r 45f85e283ce0 etc/options
--- a/etc/options	Sun May 24 09:04:25 2020 +0200
+++ b/etc/options	Sun May 24 21:11:23 2020 +0200
@@ -150,7 +150,7 @@
 
 section "PIDE Build"
 
-option pide_build : bool = false
+option pide_session : bool = false
   -- "build session heaps via PIDE"
 
 option pide_reports : bool = true
diff -r 86cfb9fa3da8 -r 45f85e283ce0 etc/settings
--- a/etc/settings	Sun May 24 09:04:25 2020 +0200
+++ b/etc/settings	Sun May 24 21:11:23 2020 +0200
@@ -23,6 +23,8 @@
 isabelle_scala_service 'isabelle.Tools'
 [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
 
+isabelle_scala_service 'isabelle.Functions'
+
 isabelle_scala_service 'isabelle.Bibtex$File_Format'
 
 #paranoia settings -- avoid intrusion of alien options
diff -r 86cfb9fa3da8 -r 45f85e283ce0 etc/symbols
--- a/etc/symbols	Sun May 24 09:04:25 2020 +0200
+++ b/etc/symbols	Sun May 24 21:11:23 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 86cfb9fa3da8 -r 45f85e283ce0 lib/Tools/scala
--- a/lib/Tools/scala	Sun May 24 09:04:25 2020 +0200
+++ b/lib/Tools/scala	Sun May 24 21:11:23 2020 +0200
@@ -13,5 +13,9 @@
   SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG"
 done
 
+[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
+unset CLASSPATH
+
 isabelle_scala scala "${SCALA_ARGS[@]}" \
-  -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
+  -classpath "$(platform_path "$ISABELLE_CLASSPATH")" \
+  -Disabelle.scala.classpath="$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff -r 86cfb9fa3da8 -r 45f85e283ce0 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Sun May 24 09:04:25 2020 +0200
+++ b/lib/texinputs/isabellesym.sty	Sun May 24 21:11:23 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 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Concurrent/future.ML	Sun May 24 21:11:23 2020 +0200
@@ -276,11 +276,9 @@
 
 fun worker_start name = (*requires SYNCHRONIZED*)
   let
-    val threads_stack_limit =
-      Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
-    val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
     val worker =
-      Isabelle_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
+      Isabelle_Thread.fork
+        {name = "worker", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false}
         (fn () => worker_loop name);
   in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
   handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Sun May 24 21:11:23 2020 +0200
@@ -8,6 +8,7 @@
 sig
   val is_self: Thread.thread -> bool
   val get_name: unit -> string
+  val stack_limit: unit -> int option
   type params = {name: string, stack_limit: int option, interrupts: bool}
   val attributes: params -> Thread.threadAttribute list
   val fork: params -> (unit -> unit) -> Thread.thread
@@ -43,6 +44,12 @@
 
 (* fork *)
 
+fun stack_limit () =
+  let
+    val threads_stack_limit =
+      Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
+  in if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit end;
+
 type params = {name: string, stack_limit: int option, interrupts: bool};
 
 fun attributes ({stack_limit, interrupts, ...}: params) =
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/General/word.scala	Sun May 24 21:11:23 2020 +0200
@@ -77,11 +77,11 @@
     explode(_ == sep, text)
 
   def explode(text: String): List[String] =
-    explode(Character.isWhitespace(_), text)
+    explode(Character.isWhitespace _, text)
 
 
   /* brackets */
 
-  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃"
-  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄"
+  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪"
+  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫"
 }
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/ML/ml_process.scala	Sun May 24 21:11:23 2020 +0200
@@ -92,8 +92,9 @@
             ML_Syntax.print_list(
               ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
 
-          List("Resources.init_session_base" +
-            " {session_positions = " + print_sessions(sessions_structure.session_positions) +
+          List("Resources.init_session" +
+            "{pide = false" +
+            ", session_positions = " + print_sessions(sessions_structure.session_positions) +
             ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
             ", docs = " + print_list(base.doc_names) +
             ", global_theories = " + print_table(base.global_theories.toList) +
@@ -112,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"))
@@ -134,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 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun May 24 21:11:23 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 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/protocol.ML	Sun May 24 21:11:23 2020 +0200
@@ -12,13 +12,17 @@
     (fn args => List.app writeln args);
 
 val _ =
+  Isabelle_Process.protocol_command "Prover.stop"
+    (fn [rc] => raise Isabelle_Process.STOP (Value.parse_int rc));
+
+val _ =
   Isabelle_Process.protocol_command "Prover.options"
     (fn [options_yxml] =>
       (Options.set_default (Options.decode (YXML.parse_body options_yxml));
        Isabelle_Process.init_options_interactive ()));
 
 val _ =
-  Isabelle_Process.protocol_command "Prover.init_session_base"
+  Isabelle_Process.protocol_command "Prover.init_session"
     (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml,
           loaded_theories_yxml] =>
       let
@@ -27,8 +31,9 @@
         val decode_sessions =
           YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
       in
-        Resources.init_session_base
-          {session_positions = decode_sessions session_positions_yxml,
+        Resources.init_session
+          {pide = true,
+           session_positions = decode_sessions session_positions_yxml,
            session_directories = decode_table session_directories_yxml,
            docs = decode_list doc_names_yxml,
            global_theories = decode_table global_theories_yxml,
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sun May 24 21:11:23 2020 +0200
@@ -328,9 +328,9 @@
     Symbol.encode_yxml(list(pair(string, properties))(lst))
   }
 
-  def session_base(resources: Resources)
+  def init_session(resources: Resources)
   {
-    protocol_command("Prover.init_session_base",
+    protocol_command("Prover.init_session",
       encode_sessions(resources.sessions_structure.session_positions),
       encode_table(resources.sessions_structure.dest_session_directories),
       encode_list(resources.session_base.doc_names),
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/resources.ML	Sun May 24 21:11:23 2020 +0200
@@ -7,13 +7,15 @@
 signature RESOURCES =
 sig
   val default_qualifier: string
-  val init_session_base:
-    {session_positions: (string * Properties.T) list,
+  val init_session:
+    {pide: bool,
+     session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
      docs: string list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
   val finish_session_base: unit -> unit
+  val is_pide: unit -> bool
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val check_session: Proof.context -> string * Position.T -> string
@@ -52,7 +54,8 @@
   {pos = Position.of_properties props, serial = serial ()};
 
 val empty_session_base =
-  {session_positions = []: (string * entry) list,
+  {pide = false,
+   session_positions = []: (string * entry) list,
    session_directories = Symtab.empty: Path.T list Symtab.table,
    docs = []: (string * entry) list,
    global_theories = Symtab.empty: string Symtab.table,
@@ -61,11 +64,12 @@
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
-fun init_session_base
-    {session_positions, session_directories, docs, global_theories, loaded_theories} =
+fun init_session
+    {pide, session_positions, session_directories, docs, global_theories, loaded_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
+      {pide = pide,
+       session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
        session_directories =
          fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
            session_directories Symtab.empty,
@@ -76,7 +80,8 @@
 fun finish_session_base () =
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
-      {session_positions = [],
+      {pide = false,
+       session_positions = [],
        session_directories = Symtab.empty,
        docs = [],
        global_theories = global_theories,
@@ -84,6 +89,8 @@
 
 fun get_session_base f = f (Synchronized.value global_session_base);
 
+fun is_pide () = get_session_base #pide;
+
 fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
 
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/PIDE/session.scala	Sun May 24 21:11:23 2020 +0200
@@ -548,7 +548,7 @@
 
             case _ if output.is_init =>
               prover.get.options(file_formats.prover_options(session_options))
-              prover.get.session_base(resources)
+              prover.get.init_session(resources)
               phase = Session.Ready
               debugger.ready()
 
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/ROOT.ML	Sun May 24 21:11:23 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 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sun May 24 21:11:23 2020 +0200
@@ -7,8 +7,7 @@
 signature ISABELLE_PROCESS =
 sig
   val is_active: unit -> bool
-  exception STOP
-  exception EXIT of int
+  exception STOP of int
   val protocol_command: string -> (string list -> unit) -> unit
   val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
@@ -36,10 +35,9 @@
 
 (* protocol commands *)
 
-exception STOP;
-exception EXIT of int;
+exception STOP of int;
 
-val is_protocol_exn = fn STOP => true | EXIT _ => true | _ => false;
+val is_protocol_exn = fn STOP _ => true | _ => false;
 
 local
 
@@ -191,7 +189,7 @@
       let
         val _ =
           (case Byte_Message.read_message in_stream of
-            NONE => raise STOP
+            NONE => raise STOP 0
           | SOME [] => Output.system_message "Isabelle process: no input"
           | SOME (name :: args) => run_command name args)
           handle exn =>
@@ -217,8 +215,7 @@
 
   in
     (case result of
-      Exn.Exn STOP => ()
-    | Exn.Exn (EXIT rc) => exit rc
+      Exn.Exn (STOP rc) => if rc = 0 then () else exit rc
     | _ => Exn.release result)
   end);
 
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun May 24 21:11:23 2020 +0200
@@ -63,95 +63,98 @@
     _services.get
   }
 
-  def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
+  def init(isabelle_root: String = "", cygwin_root: String = "")
   {
-    if (_settings.isEmpty || _services.isEmpty) {
-      val isabelle_root1 =
-        bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
+    synchronized {
+      if (_settings.isEmpty || _services.isEmpty) {
+        val isabelle_root1 =
+          bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
 
-      val cygwin_root1 =
-        if (Platform.is_windows)
-          bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
-        else ""
+        val cygwin_root1 =
+          if (Platform.is_windows)
+            bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
+          else ""
 
-      if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
+        if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
 
-      def set_cygwin_root()
-      {
-        if (Platform.is_windows)
-          _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
-      }
+        def set_cygwin_root()
+        {
+          if (Platform.is_windows)
+            _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
+        }
 
-      set_cygwin_root()
+        set_cygwin_root()
 
-      def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
-        if (env.isDefinedAt(entry._1) || entry._2 == "") env
-        else env + entry
+        def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
+          if (env.isDefinedAt(entry._1) || entry._2 == "") env
+          else env + entry
 
-      val env =
-      {
-        val temp_windows =
+        val env =
         {
-          val temp = if (Platform.is_windows) System.getenv("TEMP") else null
-          if (temp != null && temp.contains('\\')) temp else ""
+          val temp_windows =
+          {
+            val temp = if (Platform.is_windows) System.getenv("TEMP") else null
+            if (temp != null && temp.contains('\\')) temp else ""
+          }
+          val user_home = System.getProperty("user.home", "")
+          val isabelle_app = System.getProperty("isabelle.app", "")
+
+          default(
+            default(
+              default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
+                "TEMP_WINDOWS" -> temp_windows),
+              "HOME" -> user_home),
+            "ISABELLE_APP" -> "true")
         }
-        val user_home = System.getProperty("user.home", "")
-        val isabelle_app = System.getProperty("isabelle.app", "")
-
-        default(
-          default(
-            default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
-              "TEMP_WINDOWS" -> temp_windows),
-            "HOME" -> user_home),
-          "ISABELLE_APP" -> "true")
-      }
 
-      val settings =
-      {
-        val dump = JFile.createTempFile("settings", null)
-        dump.deleteOnExit
-        try {
-          val cmd1 =
-            if (Platform.is_windows)
-              List(cygwin_root1 + "\\bin\\bash", "-l",
-                File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
-            else
-              List(isabelle_root1 + "/bin/isabelle")
-          val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
+        val settings =
+        {
+          val dump = JFile.createTempFile("settings", null)
+          dump.deleteOnExit
+          try {
+            val cmd1 =
+              if (Platform.is_windows)
+                List(cygwin_root1 + "\\bin\\bash", "-l",
+                  File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
+              else
+                List(isabelle_root1 + "/bin/isabelle")
+            val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
 
-          val (output, rc) = process_output(process(cmd, env = env, redirect = true))
-          if (rc != 0) error(output)
+            val (output, rc) = process_output(process(cmd, env = env, redirect = true))
+            if (rc != 0) error(output)
 
-          val entries =
-            (for (entry <- File.read(dump).split("\u0000") if entry != "") yield {
-              val i = entry.indexOf('=')
-              if (i <= 0) entry -> ""
-              else entry.substring(0, i) -> entry.substring(i + 1)
-            }).toMap
-          entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
+            val entries =
+              (for (entry <- File.read(dump).split("\u0000") if entry != "") yield {
+                val i = entry.indexOf('=')
+                if (i <= 0) entry -> ""
+                else entry.substring(0, i) -> entry.substring(i + 1)
+              }).toMap
+            entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
+          }
+          finally { dump.delete }
         }
-        finally { dump.delete }
-      }
-      _settings = Some(settings)
-      set_cygwin_root()
+        _settings = Some(settings)
+        set_cygwin_root()
 
-      val variable = "ISABELLE_SCALA_SERVICES"
-      val services =
-        for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
-        yield {
-          def err(msg: String): Nothing =
-            error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
-          try {
-            Class.forName(name).asInstanceOf[Class[Service]]
-              .getDeclaredConstructor().newInstance()
+        val variable = "ISABELLE_SCALA_SERVICES"
+        val services =
+          for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
+          yield {
+            def err(msg: String): Nothing =
+              error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
+            try {
+              Class.forName(name).asInstanceOf[Class[Service]]
+                .getDeclaredConstructor().newInstance()
+            }
+            catch {
+              case _: ClassNotFoundException => err("Class not found")
+              case exn: Throwable => err(Exn.message(exn))
+            }
           }
-          catch {
-            case _: ClassNotFoundException => err("Class not found")
-            case exn: Throwable => err(Exn.message(exn))
-          }
-        }
-      _services = Some(services)
+        _services = Some(services)
+      }
     }
+    Scala.Compiler.default_context
   }
 
 
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/System/scala.ML	Sun May 24 21:11:23 2020 +0200
@@ -6,15 +6,17 @@
 
 signature SCALA =
 sig
-  val method: string -> string -> string
-  val promise_method: string -> string -> string future
+  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
 end;
 
 structure Scala: SCALA =
 struct
 
-(** invoke JVM method via Isabelle/Scala **)
+(** invoke Scala functions from ML **)
 
 val _ = Session.protocol_handler "isabelle.Scala";
 
@@ -27,10 +29,11 @@
   Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
 
 
-(* method invocation *)
+(* invoke function *)
 
-fun promise_method name arg =
+fun promise_function name arg =
   let
+    val _ = if Resources.is_pide () then () else raise Fail "PIDE session required";
     val id = new_id ();
     fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
     val promise = Future.promise_name "invoke_scala" abort : string future;
@@ -38,7 +41,7 @@
     val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
   in promise end;
 
-fun method name arg = Future.join (promise_method name arg);
+fun function name arg = Future.join (promise_function name arg);
 
 
 (* fulfill *)
@@ -67,4 +70,38 @@
       fulfill id tag res
         handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
 
+
+(* registered functions *)
+
+fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
+
+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;
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/System/scala.scala	Sun May 24 21:11:23 2020 +0200
@@ -7,87 +7,123 @@
 package isabelle
 
 
-import java.lang.reflect.{Method, Modifier, InvocationTargetException}
-import java.io.{File => JFile}
+import java.io.{File => JFile, StringWriter, PrintWriter}
 
-import scala.util.matching.Regex
-import scala.tools.nsc.GenericRunnerSettings
+import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
+import scala.tools.nsc.interpreter.IMain
 
 
 object Scala
 {
-  /* compiler classpath and settings */
+  /** compiler **/
 
-  def compiler_classpath(jar_dirs: List[JFile]): String =
+  object Compiler
   {
-    def find_jars(dir: JFile): List[String] =
-      File.find_files(dir, file => file.getName.endsWith(".jar")).
-        map(File.absolute_name)
+    lazy val default_context: Context = context()
+
+    def context(
+      error: String => Unit = Exn.error,
+      jar_dirs: List[JFile] = Nil): Context =
+    {
+      def find_jars(dir: JFile): List[String] =
+        File.find_files(dir, file => file.getName.endsWith(".jar")).
+          map(File.absolute_name)
+
+      val class_path =
+        for {
+          prop <- List("isabelle.scala.classpath", "java.class.path")
+          path = System.getProperty(prop, "") if path != "\"\""
+          elem <- space_explode(JFile.pathSeparatorChar, path)
+        } yield elem
+
+      val settings = new GenericRunnerSettings(error)
+      settings.classpath.value =
+        (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
+
+      new Context(settings)
+    }
+
+    def default_print_writer: PrintWriter =
+      new NewLinePrintWriter(new ConsoleWriter, true)
+
+    class Context private [Compiler](val settings: GenericRunnerSettings)
+    {
+      override def toString: String = settings.toString
 
-    val class_path =
-      space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
+      def interpreter(
+        print_writer: PrintWriter = default_print_writer,
+        class_loader: ClassLoader = null): IMain =
+      {
+        new IMain(settings, print_writer)
+        {
+          override def parentClassLoader: ClassLoader =
+            if (class_loader == null) super.parentClassLoader
+            else class_loader
+        }
+      }
 
-    (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
+      def toplevel(source: String): List[String] =
+      {
+        val out = new StringWriter
+        val interp = interpreter(new PrintWriter(out))
+        val rep = new interp.ReadEvalPrint
+        val ok = interp.withLabel("\u0001") { rep.compile(source) }
+        out.close
+
+        val Error = """(?s)^\S* error: (.*)$""".r
+        val errors =
+          space_explode('\u0001', Library.strip_ansi_color(out.toString)).
+            collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
+
+        if (!ok && errors.isEmpty) List("Error") else errors
+      }
+
+      def check(body: String): List[String] =
+      {
+        try { toplevel("package test\nobject Test { " + body + " }") }
+        catch { case ERROR(msg) => List(msg) }
+      }
+    }
   }
 
-  def compiler_settings(
-    error: String => Unit = Exn.error,
-    jar_dirs: List[JFile] = Nil): GenericRunnerSettings =
+  def check_yxml(body: String): String =
   {
-    val settings = new GenericRunnerSettings(error)
-    settings.classpath.value = compiler_classpath(jar_dirs)
-    settings
+    val errors = Compiler.default_context.check(body)
+    locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
   }
 
 
 
-  /** invoke JVM method via Isabelle/Scala **/
+  /** invoke Scala functions from ML **/
 
-  /* method reflection */
-
-  private val Ext = new Regex("(.*)\\.([^.]*)")
-  private val STRING = Class.forName("java.lang.String")
+  /* registered functions */
 
-  private def get_method(name: String): String => String =
-    name match {
-      case Ext(class_name, method_name) =>
-        val m =
-          try { Class.forName(class_name).getMethod(method_name, STRING) }
-          catch {
-            case _: ClassNotFoundException | _: NoSuchMethodException =>
-              error("No such method: " + quote(name))
-          }
-        if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
-        if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
+  sealed case class Fun(name: String, apply: String => String)
+  {
+    override def toString: String = name
+  }
 
-        (arg: String) => {
-          try { m.invoke(null, arg).asInstanceOf[String] }
-          catch {
-            case e: InvocationTargetException if e.getCause != null =>
-              throw e.getCause
-          }
-        }
-      case _ => error("Malformed method name: " + quote(name))
-    }
+  lazy val functions: List[Fun] =
+    Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten
 
 
-  /* method invocation */
+  /* invoke function */
 
   object Tag extends Enumeration
   {
     val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
-  def method(name: String, arg: String): (Tag.Value, String) =
-    Exn.capture { get_method(name) } match {
-      case Exn.Res(f) =>
-        Exn.capture { f(arg) } match {
+  def function(name: String, arg: String): (Tag.Value, String) =
+    functions.find(fun => fun.name == name) match {
+      case Some(fun) =>
+        Exn.capture { fun.apply(arg) } match {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
         }
-      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
+      case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name))
     }
 }
 
@@ -129,7 +165,7 @@
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
           Future.fork {
-            val (tag, result) = Scala.method(name, msg.text)
+            val (tag, result) = Scala.function(name, msg.text)
             fulfill(id, tag, result)
           })
         true
@@ -155,3 +191,13 @@
       Markup.Invoke_Scala.name -> invoke_scala,
       Markup.Cancel_Scala.name -> cancel_scala)
 }
+
+
+/* registered functions */
+
+class Isabelle_Scala_Functions(val functions: Scala.Fun*) extends Isabelle_System.Service
+
+class Functions extends Isabelle_Scala_Functions(
+  Scala.Fun("echo", identity),
+  Scala.Fun("scala_check", Scala.check_yxml),
+  Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))
diff -r 86cfb9fa3da8 -r 45f85e283ce0 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 21:11:23 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;
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Thy/bibtex.ML	Sun May 24 21:11:23 2020 +0200
@@ -20,7 +20,7 @@
 type message = string * Position.T;
 
 fun check_database pos0 database =
-  Scala.method "isabelle.Bibtex.check_database_yxml" 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));
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Tools/build.ML	Sun May 24 21:11:23 2020 +0200
@@ -132,7 +132,8 @@
 (* build session *)
 
 datatype args = Args of
- {symbol_codes: (string * int) list,
+ {pide: bool,
+  symbol_codes: (string * int) list,
   command_timings: Properties.T list,
   verbose: bool,
   browser_info: Path.T,
@@ -150,7 +151,7 @@
   loaded_theories: string list,
   bibtex_entries: string list};
 
-fun decode_args yxml =
+fun decode_args pide yxml =
   let
     open XML.Decode;
     val position = Position.of_properties o properties;
@@ -167,7 +168,7 @@
                   (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
       (YXML.parse_body yxml);
   in
-    Args {symbol_codes = symbol_codes, command_timings = command_timings,
+    Args {pide = pide, symbol_codes = symbol_codes, command_timings = command_timings,
       verbose = verbose, browser_info = Path.explode browser_info,
       document_files = map (apply2 Path.explode) document_files,
       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
@@ -177,15 +178,16 @@
       bibtex_entries = bibtex_entries}
   end;
 
-fun build_session (Args {symbol_codes, command_timings, verbose, browser_info, document_files,
+fun build_session (Args {pide, symbol_codes, command_timings, verbose, browser_info, document_files,
     graph_file, parent_name, chapter, session_name, master_dir, theories, session_positions,
     session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) =
   let
     val symbols = HTML.make_symbols symbol_codes;
 
     val _ =
-      Resources.init_session_base
-        {session_positions = session_positions,
+      Resources.init_session
+        {pide = pide,
+         session_positions = session_positions,
          session_directories = session_directories,
          docs = doc_names,
          global_theories = global_theories,
@@ -233,7 +235,7 @@
     val _ = SHA1.test_samples ();
     val _ = Options.load_default ();
     val _ = Isabelle_Process.init_options ();
-    val args = decode_args (File.read (Path.explode args_file));
+    val args = decode_args false (File.read (Path.explode args_file));
     val _ =
       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
         build_session args
@@ -245,25 +247,24 @@
 
 (* PIDE version *)
 
-fun build_session_finished errs =
-  XML.Encode.list XML.Encode.string errs
-  |> Output.protocol_message Markup.build_session_finished;
-
 val _ =
   Isabelle_Process.protocol_command "build_session"
     (fn [args_yxml] =>
         let
-          val args = decode_args args_yxml;
-          val errs =
-            Future.interruptible_task (fn () => (build_session args; [])) () handle exn =>
-              (Runtime.exn_message_list exn handle _ (*sic!*) =>
-                (build_session_finished ["CRASHED"];
-                  raise Isabelle_Process.EXIT 2));
-          val _ = build_session_finished errs;
+          val args = decode_args true args_yxml;
+          fun exec e =
+            if can Theory.get_pure () then
+              Isabelle_Thread.fork
+                {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (),
+                  interrupts = false} e
+              |> ignore
+            else e ();
         in
-          if null errs
-          then raise Isabelle_Process.STOP
-          else raise Isabelle_Process.EXIT 1
+          exec (fn () =>
+            (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
+              ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
+          |> let open XML.Encode in pair int (list string) end
+          |> Output.protocol_message Markup.build_session_finished)
         end
       | _ => raise Match);
 
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/Tools/build.scala	Sun May 24 21:11:23 2020 +0200
@@ -216,7 +216,7 @@
           }
           else Nil
 
-        if (options.bool("pide_build")) {
+        if (options.bool("pide_session")) {
           val resources = new Resources(sessions_structure, deps(parent))
           val session = new Session(options, resources)
 
@@ -234,15 +234,23 @@
 
               private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
               {
-                val errors =
+                val (rc, errors) =
                   try {
-                    for (err <- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text)))
-                    yield {
-                      val prt = Protocol_Message.expose_no_reports(err)
-                      Pretty.string_of(prt, metric = Symbol.Metric)
+                    val (rc, errs) =
+                    {
+                      import XML.Decode._
+                      pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
                     }
+                    val errors =
+                      for (err <- errs) yield {
+                        val prt = Protocol_Message.expose_no_reports(err)
+                        Pretty.string_of(prt, metric = Symbol.Metric)
+                      }
+                    (rc, errors)
                   }
-                  catch { case ERROR(err) => List(err) }
+                  catch { case ERROR(err) => (2, List(err)) }
+
+                session.protocol_command("Prover.stop", rc.toString)
                 build_session_errors.fulfill(errors)
                 true
               }
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Pure/library.scala
--- a/src/Pure/library.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Pure/library.scala	Sun May 24 21:11:23 2020 +0200
@@ -144,6 +144,9 @@
 
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
+  def strip_ansi_color(s: String): String =
+    s.replaceAll("""\u001b\[\d+m""", "")
+
 
   /* quote */
 
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun May 24 21:11:23 2020 +0200
@@ -25,6 +25,12 @@
 
 object JEdit_Lib
 {
+  /* jEdit directories */
+
+  def directories: List[JFile] =
+    (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_))
+
+
   /* location within multi-screen environment */
 
   final case class Screen_Location(point: Point, bounds: Rectangle)
diff -r 86cfb9fa3da8 -r 45f85e283ce0 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Sun May 24 09:04:25 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Sun May 24 21:11:23 2020 +0200
@@ -10,26 +10,12 @@
 import isabelle._
 
 import console.{Console, ConsolePane, Shell, Output}
-
-import org.gjt.sp.jedit.{jEdit, JARClassLoader}
-import org.gjt.sp.jedit.MiscUtilities
-
-import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
-
-import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
-import scala.tools.nsc.interpreter.IMain
-import scala.collection.mutable
+import org.gjt.sp.jedit.JARClassLoader
+import java.io.{OutputStream, Writer, PrintWriter}
 
 
 class Scala_Console extends Shell("Scala")
 {
-  /* reconstructed jEdit/plugin classpath */
-
-  private def jar_dirs: List[JFile] =
-    (proper_string(jEdit.getSettingsDirectory).toList :::
-     proper_string(jEdit.getJEditHome).toList).map(new JFile(_))
-
-
   /* global state -- owned by GUI thread */
 
   @volatile private var interpreters = Map.empty[Console, Interpreter]
@@ -113,12 +99,11 @@
     private val running = Synchronized[Option[Thread]](None)
     def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
 
-    private val settings = Scala.compiler_settings(error = report_error, jar_dirs = jar_dirs)
-
-    private val interp = new IMain(settings, new PrintWriter(console_writer, true))
-    {
-      override def parentClassLoader = new JARClassLoader
-    }
+    private val interp =
+      Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
+        interpreter(
+          print_writer = new PrintWriter(console_writer, true),
+          class_loader = new JARClassLoader)
 
     val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
     {