merged
authorwenzelm
Sun May 24 21:11:23 2020 +0200 (6 weeks ago)
changeset 7188545f85e283ce0
parent 71860 86cfb9fa3da8
parent 71884 2bf0283fc975
child 71886 4f4695757980
merged
     1.1 --- a/etc/options	Sun May 24 09:04:25 2020 +0200
     1.2 +++ b/etc/options	Sun May 24 21:11:23 2020 +0200
     1.3 @@ -150,7 +150,7 @@
     1.4  
     1.5  section "PIDE Build"
     1.6  
     1.7 -option pide_build : bool = false
     1.8 +option pide_session : bool = false
     1.9    -- "build session heaps via PIDE"
    1.10  
    1.11  option pide_reports : bool = true
     2.1 --- a/etc/settings	Sun May 24 09:04:25 2020 +0200
     2.2 +++ b/etc/settings	Sun May 24 21:11:23 2020 +0200
     2.3 @@ -23,6 +23,8 @@
     2.4  isabelle_scala_service 'isabelle.Tools'
     2.5  [ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
     2.6  
     2.7 +isabelle_scala_service 'isabelle.Functions'
     2.8 +
     2.9  isabelle_scala_service 'isabelle.Bibtex$File_Format'
    2.10  
    2.11  #paranoia settings -- avoid intrusion of alien options
     3.1 --- a/etc/symbols	Sun May 24 09:04:25 2020 +0200
     3.2 +++ b/etc/symbols	Sun May 24 21:11:23 2020 +0200
     3.3 @@ -417,6 +417,8 @@
     3.4  \<^plugin>              argument: cartouche
     3.5  \<^print>
     3.6  \<^prop>                argument: cartouche
     3.7 +\<^scala>               argument: cartouche
     3.8 +\<^scala_function>      argument: cartouche
     3.9  \<^session>             argument: cartouche
    3.10  \<^simproc>             argument: cartouche
    3.11  \<^sort>                argument: cartouche
     4.1 --- a/lib/Tools/scala	Sun May 24 09:04:25 2020 +0200
     4.2 +++ b/lib/Tools/scala	Sun May 24 21:11:23 2020 +0200
     4.3 @@ -13,5 +13,9 @@
     4.4    SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG"
     4.5  done
     4.6  
     4.7 +[ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
     4.8 +unset CLASSPATH
     4.9 +
    4.10  isabelle_scala scala "${SCALA_ARGS[@]}" \
    4.11 -  -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
    4.12 +  -classpath "$(platform_path "$ISABELLE_CLASSPATH")" \
    4.13 +  -Disabelle.scala.classpath="$(platform_path "$ISABELLE_CLASSPATH")" "$@"
     5.1 --- a/lib/texinputs/isabellesym.sty	Sun May 24 09:04:25 2020 +0200
     5.2 +++ b/lib/texinputs/isabellesym.sty	Sun May 24 21:11:23 2020 +0200
     5.3 @@ -402,6 +402,8 @@
     5.4  \newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}}
     5.5  \newcommand{\isactrlprint}{\isakeywordcontrol{print}}
     5.6  \newcommand{\isactrlprop}{\isakeywordcontrol{prop}}
     5.7 +\newcommand{\isactrlscala}{\isakeywordcontrol{scala}}
     5.8 +\newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}}
     5.9  \newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}}
    5.10  \newcommand{\isactrlsort}{\isakeywordcontrol{sort}}
    5.11  \newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}}
     6.1 --- a/src/Pure/Concurrent/future.ML	Sun May 24 09:04:25 2020 +0200
     6.2 +++ b/src/Pure/Concurrent/future.ML	Sun May 24 21:11:23 2020 +0200
     6.3 @@ -276,11 +276,9 @@
     6.4  
     6.5  fun worker_start name = (*requires SYNCHRONIZED*)
     6.6    let
     6.7 -    val threads_stack_limit =
     6.8 -      Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
     6.9 -    val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
    6.10      val worker =
    6.11 -      Isabelle_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
    6.12 +      Isabelle_Thread.fork
    6.13 +        {name = "worker", stack_limit = Isabelle_Thread.stack_limit (), interrupts = false}
    6.14          (fn () => worker_loop name);
    6.15    in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
    6.16    handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
     7.1 --- a/src/Pure/Concurrent/isabelle_thread.ML	Sun May 24 09:04:25 2020 +0200
     7.2 +++ b/src/Pure/Concurrent/isabelle_thread.ML	Sun May 24 21:11:23 2020 +0200
     7.3 @@ -8,6 +8,7 @@
     7.4  sig
     7.5    val is_self: Thread.thread -> bool
     7.6    val get_name: unit -> string
     7.7 +  val stack_limit: unit -> int option
     7.8    type params = {name: string, stack_limit: int option, interrupts: bool}
     7.9    val attributes: params -> Thread.threadAttribute list
    7.10    val fork: params -> (unit -> unit) -> Thread.thread
    7.11 @@ -43,6 +44,12 @@
    7.12  
    7.13  (* fork *)
    7.14  
    7.15 +fun stack_limit () =
    7.16 +  let
    7.17 +    val threads_stack_limit =
    7.18 +      Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
    7.19 +  in if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit end;
    7.20 +
    7.21  type params = {name: string, stack_limit: int option, interrupts: bool};
    7.22  
    7.23  fun attributes ({stack_limit, interrupts, ...}: params) =
     8.1 --- a/src/Pure/General/word.scala	Sun May 24 09:04:25 2020 +0200
     8.2 +++ b/src/Pure/General/word.scala	Sun May 24 21:11:23 2020 +0200
     8.3 @@ -77,11 +77,11 @@
     8.4      explode(_ == sep, text)
     8.5  
     8.6    def explode(text: String): List[String] =
     8.7 -    explode(Character.isWhitespace(_), text)
     8.8 +    explode(Character.isWhitespace _, text)
     8.9  
    8.10  
    8.11    /* brackets */
    8.12  
    8.13 -  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃"
    8.14 -  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄"
    8.15 +  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪"
    8.16 +  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫"
    8.17  }
     9.1 --- a/src/Pure/ML/ml_process.scala	Sun May 24 09:04:25 2020 +0200
     9.2 +++ b/src/Pure/ML/ml_process.scala	Sun May 24 21:11:23 2020 +0200
     9.3 @@ -92,8 +92,9 @@
     9.4              ML_Syntax.print_list(
     9.5                ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list)
     9.6  
     9.7 -          List("Resources.init_session_base" +
     9.8 -            " {session_positions = " + print_sessions(sessions_structure.session_positions) +
     9.9 +          List("Resources.init_session" +
    9.10 +            "{pide = false" +
    9.11 +            ", session_positions = " + print_sessions(sessions_structure.session_positions) +
    9.12              ", session_directories = " + print_table(sessions_structure.dest_session_directories) +
    9.13              ", docs = " + print_list(base.doc_names) +
    9.14              ", global_theories = " + print_table(base.global_theories.toList) +
    9.15 @@ -112,6 +113,8 @@
    9.16      val isabelle_tmp = Isabelle_System.tmp_dir("process")
    9.17      val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
    9.18  
    9.19 +    val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(","))
    9.20 +
    9.21      val ml_runtime_options =
    9.22      {
    9.23        val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
    9.24 @@ -134,7 +137,7 @@
    9.25        "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
    9.26          Bash.strings(bash_args),
    9.27        cwd = cwd,
    9.28 -      env = env ++ env_options ++ env_tmp,
    9.29 +      env = env ++ env_options ++ env_tmp ++ env_functions,
    9.30        redirect = redirect,
    9.31        cleanup = () =>
    9.32          {
    10.1 --- a/src/Pure/PIDE/markup.ML	Sun May 24 09:04:25 2020 +0200
    10.2 +++ b/src/Pure/PIDE/markup.ML	Sun May 24 21:11:23 2020 +0200
    10.3 @@ -68,6 +68,7 @@
    10.4    val export_pathN: string val export_path: string -> T
    10.5    val urlN: string val url: string -> T
    10.6    val docN: string val doc: string -> T
    10.7 +  val scala_functionN: string val scala_function: string -> T
    10.8    val markupN: string
    10.9    val consistentN: string
   10.10    val unbreakableN: string
   10.11 @@ -405,6 +406,7 @@
   10.12  val (export_pathN, export_path) = markup_string "export_path" nameN;
   10.13  val (urlN, url) = markup_string "url" nameN;
   10.14  val (docN, doc) = markup_string "doc" nameN;
   10.15 +val (scala_functionN, scala_function) = markup_string "scala_function" nameN;
   10.16  
   10.17  
   10.18  (* pretty printing *)
    11.1 --- a/src/Pure/PIDE/protocol.ML	Sun May 24 09:04:25 2020 +0200
    11.2 +++ b/src/Pure/PIDE/protocol.ML	Sun May 24 21:11:23 2020 +0200
    11.3 @@ -12,13 +12,17 @@
    11.4      (fn args => List.app writeln args);
    11.5  
    11.6  val _ =
    11.7 +  Isabelle_Process.protocol_command "Prover.stop"
    11.8 +    (fn [rc] => raise Isabelle_Process.STOP (Value.parse_int rc));
    11.9 +
   11.10 +val _ =
   11.11    Isabelle_Process.protocol_command "Prover.options"
   11.12      (fn [options_yxml] =>
   11.13        (Options.set_default (Options.decode (YXML.parse_body options_yxml));
   11.14         Isabelle_Process.init_options_interactive ()));
   11.15  
   11.16  val _ =
   11.17 -  Isabelle_Process.protocol_command "Prover.init_session_base"
   11.18 +  Isabelle_Process.protocol_command "Prover.init_session"
   11.19      (fn [session_positions_yxml, session_directories_yxml, doc_names_yxml, global_theories_yxml,
   11.20            loaded_theories_yxml] =>
   11.21        let
   11.22 @@ -27,8 +31,9 @@
   11.23          val decode_sessions =
   11.24            YXML.parse_body #> let open XML.Decode in list (pair string properties) end;
   11.25        in
   11.26 -        Resources.init_session_base
   11.27 -          {session_positions = decode_sessions session_positions_yxml,
   11.28 +        Resources.init_session
   11.29 +          {pide = true,
   11.30 +           session_positions = decode_sessions session_positions_yxml,
   11.31             session_directories = decode_table session_directories_yxml,
   11.32             docs = decode_list doc_names_yxml,
   11.33             global_theories = decode_table global_theories_yxml,
    12.1 --- a/src/Pure/PIDE/protocol.scala	Sun May 24 09:04:25 2020 +0200
    12.2 +++ b/src/Pure/PIDE/protocol.scala	Sun May 24 21:11:23 2020 +0200
    12.3 @@ -328,9 +328,9 @@
    12.4      Symbol.encode_yxml(list(pair(string, properties))(lst))
    12.5    }
    12.6  
    12.7 -  def session_base(resources: Resources)
    12.8 +  def init_session(resources: Resources)
    12.9    {
   12.10 -    protocol_command("Prover.init_session_base",
   12.11 +    protocol_command("Prover.init_session",
   12.12        encode_sessions(resources.sessions_structure.session_positions),
   12.13        encode_table(resources.sessions_structure.dest_session_directories),
   12.14        encode_list(resources.session_base.doc_names),
    13.1 --- a/src/Pure/PIDE/resources.ML	Sun May 24 09:04:25 2020 +0200
    13.2 +++ b/src/Pure/PIDE/resources.ML	Sun May 24 21:11:23 2020 +0200
    13.3 @@ -7,13 +7,15 @@
    13.4  signature RESOURCES =
    13.5  sig
    13.6    val default_qualifier: string
    13.7 -  val init_session_base:
    13.8 -    {session_positions: (string * Properties.T) list,
    13.9 +  val init_session:
   13.10 +    {pide: bool,
   13.11 +     session_positions: (string * Properties.T) list,
   13.12       session_directories: (string * string) list,
   13.13       docs: string list,
   13.14       global_theories: (string * string) list,
   13.15       loaded_theories: string list} -> unit
   13.16    val finish_session_base: unit -> unit
   13.17 +  val is_pide: unit -> bool
   13.18    val global_theory: string -> string option
   13.19    val loaded_theory: string -> bool
   13.20    val check_session: Proof.context -> string * Position.T -> string
   13.21 @@ -52,7 +54,8 @@
   13.22    {pos = Position.of_properties props, serial = serial ()};
   13.23  
   13.24  val empty_session_base =
   13.25 -  {session_positions = []: (string * entry) list,
   13.26 +  {pide = false,
   13.27 +   session_positions = []: (string * entry) list,
   13.28     session_directories = Symtab.empty: Path.T list Symtab.table,
   13.29     docs = []: (string * entry) list,
   13.30     global_theories = Symtab.empty: string Symtab.table,
   13.31 @@ -61,11 +64,12 @@
   13.32  val global_session_base =
   13.33    Synchronized.var "Sessions.base" empty_session_base;
   13.34  
   13.35 -fun init_session_base
   13.36 -    {session_positions, session_directories, docs, global_theories, loaded_theories} =
   13.37 +fun init_session
   13.38 +    {pide, session_positions, session_directories, docs, global_theories, loaded_theories} =
   13.39    Synchronized.change global_session_base
   13.40      (fn _ =>
   13.41 -      {session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
   13.42 +      {pide = pide,
   13.43 +       session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
   13.44         session_directories =
   13.45           fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
   13.46             session_directories Symtab.empty,
   13.47 @@ -76,7 +80,8 @@
   13.48  fun finish_session_base () =
   13.49    Synchronized.change global_session_base
   13.50      (fn {global_theories, loaded_theories, ...} =>
   13.51 -      {session_positions = [],
   13.52 +      {pide = false,
   13.53 +       session_positions = [],
   13.54         session_directories = Symtab.empty,
   13.55         docs = [],
   13.56         global_theories = global_theories,
   13.57 @@ -84,6 +89,8 @@
   13.58  
   13.59  fun get_session_base f = f (Synchronized.value global_session_base);
   13.60  
   13.61 +fun is_pide () = get_session_base #pide;
   13.62 +
   13.63  fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
   13.64  fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
   13.65  
    14.1 --- a/src/Pure/PIDE/session.scala	Sun May 24 09:04:25 2020 +0200
    14.2 +++ b/src/Pure/PIDE/session.scala	Sun May 24 21:11:23 2020 +0200
    14.3 @@ -548,7 +548,7 @@
    14.4  
    14.5              case _ if output.is_init =>
    14.6                prover.get.options(file_formats.prover_options(session_options))
    14.7 -              prover.get.session_base(resources)
    14.8 +              prover.get.init_session(resources)
    14.9                phase = Session.Ready
   14.10                debugger.ready()
   14.11  
    15.1 --- a/src/Pure/ROOT.ML	Sun May 24 09:04:25 2020 +0200
    15.2 +++ b/src/Pure/ROOT.ML	Sun May 24 21:11:23 2020 +0200
    15.3 @@ -328,6 +328,7 @@
    15.4  ML_file "System/message_channel.ML";
    15.5  ML_file "System/isabelle_process.ML";
    15.6  ML_file "System/scala.ML";
    15.7 +ML_file "System/scala_check.ML";
    15.8  ML_file "Thy/bibtex.ML";
    15.9  ML_file "PIDE/protocol.ML";
   15.10  ML_file "General/output_primitives_virtual.ML";
    16.1 --- a/src/Pure/System/isabelle_process.ML	Sun May 24 09:04:25 2020 +0200
    16.2 +++ b/src/Pure/System/isabelle_process.ML	Sun May 24 21:11:23 2020 +0200
    16.3 @@ -7,8 +7,7 @@
    16.4  signature ISABELLE_PROCESS =
    16.5  sig
    16.6    val is_active: unit -> bool
    16.7 -  exception STOP
    16.8 -  exception EXIT of int
    16.9 +  exception STOP of int
   16.10    val protocol_command: string -> (string list -> unit) -> unit
   16.11    val reset_tracing: Document_ID.exec -> unit
   16.12    val crashes: exn list Synchronized.var
   16.13 @@ -36,10 +35,9 @@
   16.14  
   16.15  (* protocol commands *)
   16.16  
   16.17 -exception STOP;
   16.18 -exception EXIT of int;
   16.19 +exception STOP of int;
   16.20  
   16.21 -val is_protocol_exn = fn STOP => true | EXIT _ => true | _ => false;
   16.22 +val is_protocol_exn = fn STOP _ => true | _ => false;
   16.23  
   16.24  local
   16.25  
   16.26 @@ -191,7 +189,7 @@
   16.27        let
   16.28          val _ =
   16.29            (case Byte_Message.read_message in_stream of
   16.30 -            NONE => raise STOP
   16.31 +            NONE => raise STOP 0
   16.32            | SOME [] => Output.system_message "Isabelle process: no input"
   16.33            | SOME (name :: args) => run_command name args)
   16.34            handle exn =>
   16.35 @@ -217,8 +215,7 @@
   16.36  
   16.37    in
   16.38      (case result of
   16.39 -      Exn.Exn STOP => ()
   16.40 -    | Exn.Exn (EXIT rc) => exit rc
   16.41 +      Exn.Exn (STOP rc) => if rc = 0 then () else exit rc
   16.42      | _ => Exn.release result)
   16.43    end);
   16.44  
    17.1 --- a/src/Pure/System/isabelle_system.scala	Sun May 24 09:04:25 2020 +0200
    17.2 +++ b/src/Pure/System/isabelle_system.scala	Sun May 24 21:11:23 2020 +0200
    17.3 @@ -63,95 +63,98 @@
    17.4      _services.get
    17.5    }
    17.6  
    17.7 -  def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
    17.8 +  def init(isabelle_root: String = "", cygwin_root: String = "")
    17.9    {
   17.10 -    if (_settings.isEmpty || _services.isEmpty) {
   17.11 -      val isabelle_root1 =
   17.12 -        bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
   17.13 +    synchronized {
   17.14 +      if (_settings.isEmpty || _services.isEmpty) {
   17.15 +        val isabelle_root1 =
   17.16 +          bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
   17.17  
   17.18 -      val cygwin_root1 =
   17.19 -        if (Platform.is_windows)
   17.20 -          bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
   17.21 -        else ""
   17.22 +        val cygwin_root1 =
   17.23 +          if (Platform.is_windows)
   17.24 +            bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
   17.25 +          else ""
   17.26  
   17.27 -      if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
   17.28 +        if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
   17.29  
   17.30 -      def set_cygwin_root()
   17.31 -      {
   17.32 -        if (Platform.is_windows)
   17.33 -          _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
   17.34 -      }
   17.35 +        def set_cygwin_root()
   17.36 +        {
   17.37 +          if (Platform.is_windows)
   17.38 +            _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
   17.39 +        }
   17.40  
   17.41 -      set_cygwin_root()
   17.42 +        set_cygwin_root()
   17.43  
   17.44 -      def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
   17.45 -        if (env.isDefinedAt(entry._1) || entry._2 == "") env
   17.46 -        else env + entry
   17.47 +        def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
   17.48 +          if (env.isDefinedAt(entry._1) || entry._2 == "") env
   17.49 +          else env + entry
   17.50  
   17.51 -      val env =
   17.52 -      {
   17.53 -        val temp_windows =
   17.54 +        val env =
   17.55          {
   17.56 -          val temp = if (Platform.is_windows) System.getenv("TEMP") else null
   17.57 -          if (temp != null && temp.contains('\\')) temp else ""
   17.58 +          val temp_windows =
   17.59 +          {
   17.60 +            val temp = if (Platform.is_windows) System.getenv("TEMP") else null
   17.61 +            if (temp != null && temp.contains('\\')) temp else ""
   17.62 +          }
   17.63 +          val user_home = System.getProperty("user.home", "")
   17.64 +          val isabelle_app = System.getProperty("isabelle.app", "")
   17.65 +
   17.66 +          default(
   17.67 +            default(
   17.68 +              default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
   17.69 +                "TEMP_WINDOWS" -> temp_windows),
   17.70 +              "HOME" -> user_home),
   17.71 +            "ISABELLE_APP" -> "true")
   17.72          }
   17.73 -        val user_home = System.getProperty("user.home", "")
   17.74 -        val isabelle_app = System.getProperty("isabelle.app", "")
   17.75 -
   17.76 -        default(
   17.77 -          default(
   17.78 -            default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
   17.79 -              "TEMP_WINDOWS" -> temp_windows),
   17.80 -            "HOME" -> user_home),
   17.81 -          "ISABELLE_APP" -> "true")
   17.82 -      }
   17.83  
   17.84 -      val settings =
   17.85 -      {
   17.86 -        val dump = JFile.createTempFile("settings", null)
   17.87 -        dump.deleteOnExit
   17.88 -        try {
   17.89 -          val cmd1 =
   17.90 -            if (Platform.is_windows)
   17.91 -              List(cygwin_root1 + "\\bin\\bash", "-l",
   17.92 -                File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
   17.93 -            else
   17.94 -              List(isabelle_root1 + "/bin/isabelle")
   17.95 -          val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
   17.96 +        val settings =
   17.97 +        {
   17.98 +          val dump = JFile.createTempFile("settings", null)
   17.99 +          dump.deleteOnExit
  17.100 +          try {
  17.101 +            val cmd1 =
  17.102 +              if (Platform.is_windows)
  17.103 +                List(cygwin_root1 + "\\bin\\bash", "-l",
  17.104 +                  File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
  17.105 +              else
  17.106 +                List(isabelle_root1 + "/bin/isabelle")
  17.107 +            val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
  17.108  
  17.109 -          val (output, rc) = process_output(process(cmd, env = env, redirect = true))
  17.110 -          if (rc != 0) error(output)
  17.111 +            val (output, rc) = process_output(process(cmd, env = env, redirect = true))
  17.112 +            if (rc != 0) error(output)
  17.113  
  17.114 -          val entries =
  17.115 -            (for (entry <- File.read(dump).split("\u0000") if entry != "") yield {
  17.116 -              val i = entry.indexOf('=')
  17.117 -              if (i <= 0) entry -> ""
  17.118 -              else entry.substring(0, i) -> entry.substring(i + 1)
  17.119 -            }).toMap
  17.120 -          entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
  17.121 +            val entries =
  17.122 +              (for (entry <- File.read(dump).split("\u0000") if entry != "") yield {
  17.123 +                val i = entry.indexOf('=')
  17.124 +                if (i <= 0) entry -> ""
  17.125 +                else entry.substring(0, i) -> entry.substring(i + 1)
  17.126 +              }).toMap
  17.127 +            entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
  17.128 +          }
  17.129 +          finally { dump.delete }
  17.130          }
  17.131 -        finally { dump.delete }
  17.132 -      }
  17.133 -      _settings = Some(settings)
  17.134 -      set_cygwin_root()
  17.135 +        _settings = Some(settings)
  17.136 +        set_cygwin_root()
  17.137  
  17.138 -      val variable = "ISABELLE_SCALA_SERVICES"
  17.139 -      val services =
  17.140 -        for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
  17.141 -        yield {
  17.142 -          def err(msg: String): Nothing =
  17.143 -            error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
  17.144 -          try {
  17.145 -            Class.forName(name).asInstanceOf[Class[Service]]
  17.146 -              .getDeclaredConstructor().newInstance()
  17.147 +        val variable = "ISABELLE_SCALA_SERVICES"
  17.148 +        val services =
  17.149 +          for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
  17.150 +          yield {
  17.151 +            def err(msg: String): Nothing =
  17.152 +              error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
  17.153 +            try {
  17.154 +              Class.forName(name).asInstanceOf[Class[Service]]
  17.155 +                .getDeclaredConstructor().newInstance()
  17.156 +            }
  17.157 +            catch {
  17.158 +              case _: ClassNotFoundException => err("Class not found")
  17.159 +              case exn: Throwable => err(Exn.message(exn))
  17.160 +            }
  17.161            }
  17.162 -          catch {
  17.163 -            case _: ClassNotFoundException => err("Class not found")
  17.164 -            case exn: Throwable => err(Exn.message(exn))
  17.165 -          }
  17.166 -        }
  17.167 -      _services = Some(services)
  17.168 +        _services = Some(services)
  17.169 +      }
  17.170      }
  17.171 +    Scala.Compiler.default_context
  17.172    }
  17.173  
  17.174  
    18.1 --- a/src/Pure/System/scala.ML	Sun May 24 09:04:25 2020 +0200
    18.2 +++ b/src/Pure/System/scala.ML	Sun May 24 21:11:23 2020 +0200
    18.3 @@ -6,15 +6,17 @@
    18.4  
    18.5  signature SCALA =
    18.6  sig
    18.7 -  val method: string -> string -> string
    18.8 -  val promise_method: string -> string -> string future
    18.9 +  val functions: unit -> string list
   18.10 +  val check_function: Proof.context -> string * Position.T -> string
   18.11 +  val promise_function: string -> string -> string future
   18.12 +  val function: string -> string -> string
   18.13    exception Null
   18.14  end;
   18.15  
   18.16  structure Scala: SCALA =
   18.17  struct
   18.18  
   18.19 -(** invoke JVM method via Isabelle/Scala **)
   18.20 +(** invoke Scala functions from ML **)
   18.21  
   18.22  val _ = Session.protocol_handler "isabelle.Scala";
   18.23  
   18.24 @@ -27,10 +29,11 @@
   18.25    Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table);
   18.26  
   18.27  
   18.28 -(* method invocation *)
   18.29 +(* invoke function *)
   18.30  
   18.31 -fun promise_method name arg =
   18.32 +fun promise_function name arg =
   18.33    let
   18.34 +    val _ = if Resources.is_pide () then () else raise Fail "PIDE session required";
   18.35      val id = new_id ();
   18.36      fun abort () = Output.protocol_message (Markup.cancel_scala id) [];
   18.37      val promise = Future.promise_name "invoke_scala" abort : string future;
   18.38 @@ -38,7 +41,7 @@
   18.39      val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg];
   18.40    in promise end;
   18.41  
   18.42 -fun method name arg = Future.join (promise_method name arg);
   18.43 +fun function name arg = Future.join (promise_function name arg);
   18.44  
   18.45  
   18.46  (* fulfill *)
   18.47 @@ -67,4 +70,38 @@
   18.48        fulfill id tag res
   18.49          handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
   18.50  
   18.51 +
   18.52 +(* registered functions *)
   18.53 +
   18.54 +fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
   18.55 +
   18.56 +fun check_function ctxt (name, pos) =
   18.57 +  let
   18.58 +    val kind = Markup.scala_functionN;
   18.59 +    val funs = functions ();
   18.60 +  in
   18.61 +    if member (op =) funs name then
   18.62 +      (Context_Position.report ctxt pos (Markup.scala_function name); name)
   18.63 +    else
   18.64 +      let
   18.65 +        val completion_report =
   18.66 +          Completion.make_report (name, pos)
   18.67 +            (fn completed =>
   18.68 +              filter completed funs
   18.69 +              |> sort_strings
   18.70 +              |> map (fn a => (a, (kind, a))));
   18.71 +      in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end
   18.72 +  end;
   18.73 +
   18.74 +val _ = Theory.setup
   18.75 + (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
   18.76 +    (Scan.lift Parse.embedded_position) check_function #>
   18.77 +  ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
   18.78 +    (Args.context -- Scan.lift Parse.embedded_position
   18.79 +      >> (uncurry check_function #> ML_Syntax.print_string)) #>
   18.80 +  ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
   18.81 +    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
   18.82 +      let val name = check_function ctxt arg
   18.83 +      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)));
   18.84 +
   18.85  end;
    19.1 --- a/src/Pure/System/scala.scala	Sun May 24 09:04:25 2020 +0200
    19.2 +++ b/src/Pure/System/scala.scala	Sun May 24 21:11:23 2020 +0200
    19.3 @@ -7,87 +7,123 @@
    19.4  package isabelle
    19.5  
    19.6  
    19.7 -import java.lang.reflect.{Method, Modifier, InvocationTargetException}
    19.8 -import java.io.{File => JFile}
    19.9 +import java.io.{File => JFile, StringWriter, PrintWriter}
   19.10  
   19.11 -import scala.util.matching.Regex
   19.12 -import scala.tools.nsc.GenericRunnerSettings
   19.13 +import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
   19.14 +import scala.tools.nsc.interpreter.IMain
   19.15  
   19.16  
   19.17  object Scala
   19.18  {
   19.19 -  /* compiler classpath and settings */
   19.20 +  /** compiler **/
   19.21  
   19.22 -  def compiler_classpath(jar_dirs: List[JFile]): String =
   19.23 +  object Compiler
   19.24    {
   19.25 -    def find_jars(dir: JFile): List[String] =
   19.26 -      File.find_files(dir, file => file.getName.endsWith(".jar")).
   19.27 -        map(File.absolute_name)
   19.28 +    lazy val default_context: Context = context()
   19.29 +
   19.30 +    def context(
   19.31 +      error: String => Unit = Exn.error,
   19.32 +      jar_dirs: List[JFile] = Nil): Context =
   19.33 +    {
   19.34 +      def find_jars(dir: JFile): List[String] =
   19.35 +        File.find_files(dir, file => file.getName.endsWith(".jar")).
   19.36 +          map(File.absolute_name)
   19.37 +
   19.38 +      val class_path =
   19.39 +        for {
   19.40 +          prop <- List("isabelle.scala.classpath", "java.class.path")
   19.41 +          path = System.getProperty(prop, "") if path != "\"\""
   19.42 +          elem <- space_explode(JFile.pathSeparatorChar, path)
   19.43 +        } yield elem
   19.44 +
   19.45 +      val settings = new GenericRunnerSettings(error)
   19.46 +      settings.classpath.value =
   19.47 +        (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
   19.48 +
   19.49 +      new Context(settings)
   19.50 +    }
   19.51 +
   19.52 +    def default_print_writer: PrintWriter =
   19.53 +      new NewLinePrintWriter(new ConsoleWriter, true)
   19.54 +
   19.55 +    class Context private [Compiler](val settings: GenericRunnerSettings)
   19.56 +    {
   19.57 +      override def toString: String = settings.toString
   19.58  
   19.59 -    val class_path =
   19.60 -      space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
   19.61 +      def interpreter(
   19.62 +        print_writer: PrintWriter = default_print_writer,
   19.63 +        class_loader: ClassLoader = null): IMain =
   19.64 +      {
   19.65 +        new IMain(settings, print_writer)
   19.66 +        {
   19.67 +          override def parentClassLoader: ClassLoader =
   19.68 +            if (class_loader == null) super.parentClassLoader
   19.69 +            else class_loader
   19.70 +        }
   19.71 +      }
   19.72  
   19.73 -    (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
   19.74 +      def toplevel(source: String): List[String] =
   19.75 +      {
   19.76 +        val out = new StringWriter
   19.77 +        val interp = interpreter(new PrintWriter(out))
   19.78 +        val rep = new interp.ReadEvalPrint
   19.79 +        val ok = interp.withLabel("\u0001") { rep.compile(source) }
   19.80 +        out.close
   19.81 +
   19.82 +        val Error = """(?s)^\S* error: (.*)$""".r
   19.83 +        val errors =
   19.84 +          space_explode('\u0001', Library.strip_ansi_color(out.toString)).
   19.85 +            collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
   19.86 +
   19.87 +        if (!ok && errors.isEmpty) List("Error") else errors
   19.88 +      }
   19.89 +
   19.90 +      def check(body: String): List[String] =
   19.91 +      {
   19.92 +        try { toplevel("package test\nobject Test { " + body + " }") }
   19.93 +        catch { case ERROR(msg) => List(msg) }
   19.94 +      }
   19.95 +    }
   19.96    }
   19.97  
   19.98 -  def compiler_settings(
   19.99 -    error: String => Unit = Exn.error,
  19.100 -    jar_dirs: List[JFile] = Nil): GenericRunnerSettings =
  19.101 +  def check_yxml(body: String): String =
  19.102    {
  19.103 -    val settings = new GenericRunnerSettings(error)
  19.104 -    settings.classpath.value = compiler_classpath(jar_dirs)
  19.105 -    settings
  19.106 +    val errors = Compiler.default_context.check(body)
  19.107 +    locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
  19.108    }
  19.109  
  19.110  
  19.111  
  19.112 -  /** invoke JVM method via Isabelle/Scala **/
  19.113 +  /** invoke Scala functions from ML **/
  19.114  
  19.115 -  /* method reflection */
  19.116 -
  19.117 -  private val Ext = new Regex("(.*)\\.([^.]*)")
  19.118 -  private val STRING = Class.forName("java.lang.String")
  19.119 +  /* registered functions */
  19.120  
  19.121 -  private def get_method(name: String): String => String =
  19.122 -    name match {
  19.123 -      case Ext(class_name, method_name) =>
  19.124 -        val m =
  19.125 -          try { Class.forName(class_name).getMethod(method_name, STRING) }
  19.126 -          catch {
  19.127 -            case _: ClassNotFoundException | _: NoSuchMethodException =>
  19.128 -              error("No such method: " + quote(name))
  19.129 -          }
  19.130 -        if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
  19.131 -        if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
  19.132 +  sealed case class Fun(name: String, apply: String => String)
  19.133 +  {
  19.134 +    override def toString: String = name
  19.135 +  }
  19.136  
  19.137 -        (arg: String) => {
  19.138 -          try { m.invoke(null, arg).asInstanceOf[String] }
  19.139 -          catch {
  19.140 -            case e: InvocationTargetException if e.getCause != null =>
  19.141 -              throw e.getCause
  19.142 -          }
  19.143 -        }
  19.144 -      case _ => error("Malformed method name: " + quote(name))
  19.145 -    }
  19.146 +  lazy val functions: List[Fun] =
  19.147 +    Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten
  19.148  
  19.149  
  19.150 -  /* method invocation */
  19.151 +  /* invoke function */
  19.152  
  19.153    object Tag extends Enumeration
  19.154    {
  19.155      val NULL, OK, ERROR, FAIL, INTERRUPT = Value
  19.156    }
  19.157  
  19.158 -  def method(name: String, arg: String): (Tag.Value, String) =
  19.159 -    Exn.capture { get_method(name) } match {
  19.160 -      case Exn.Res(f) =>
  19.161 -        Exn.capture { f(arg) } match {
  19.162 +  def function(name: String, arg: String): (Tag.Value, String) =
  19.163 +    functions.find(fun => fun.name == name) match {
  19.164 +      case Some(fun) =>
  19.165 +        Exn.capture { fun.apply(arg) } match {
  19.166            case Exn.Res(null) => (Tag.NULL, "")
  19.167            case Exn.Res(res) => (Tag.OK, res)
  19.168            case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
  19.169            case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
  19.170          }
  19.171 -      case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
  19.172 +      case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name))
  19.173      }
  19.174  }
  19.175  
  19.176 @@ -129,7 +165,7 @@
  19.177        case Markup.Invoke_Scala(name, id) =>
  19.178          futures += (id ->
  19.179            Future.fork {
  19.180 -            val (tag, result) = Scala.method(name, msg.text)
  19.181 +            val (tag, result) = Scala.function(name, msg.text)
  19.182              fulfill(id, tag, result)
  19.183            })
  19.184          true
  19.185 @@ -155,3 +191,13 @@
  19.186        Markup.Invoke_Scala.name -> invoke_scala,
  19.187        Markup.Cancel_Scala.name -> cancel_scala)
  19.188  }
  19.189 +
  19.190 +
  19.191 +/* registered functions */
  19.192 +
  19.193 +class Isabelle_Scala_Functions(val functions: Scala.Fun*) extends Isabelle_System.Service
  19.194 +
  19.195 +class Functions extends Isabelle_Scala_Functions(
  19.196 +  Scala.Fun("echo", identity),
  19.197 +  Scala.Fun("scala_check", Scala.check_yxml),
  19.198 +  Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml))
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/Pure/System/scala_check.ML	Sun May 24 21:11:23 2020 +0200
    20.3 @@ -0,0 +1,22 @@
    20.4 +(*  Title:      Pure/System/scala_check.ML
    20.5 +    Author:     Makarius
    20.6 +
    20.7 +Semantic check of Scala sources.
    20.8 +*)
    20.9 +
   20.10 +signature SCALA_CHECK =
   20.11 +sig
   20.12 +  val decl: string -> unit
   20.13 +end;
   20.14 +
   20.15 +structure Scala_Check: SCALA_CHECK =
   20.16 +struct
   20.17 +
   20.18 +fun decl source =
   20.19 +  let val errors =
   20.20 +    \<^scala>\<open>scala_check\<close> source
   20.21 +    |> YXML.parse_body
   20.22 +    |> let open XML.Decode in list string end
   20.23 +  in if null errors then () else error (cat_lines errors) end;
   20.24 +
   20.25 +end;
    21.1 --- a/src/Pure/Thy/bibtex.ML	Sun May 24 09:04:25 2020 +0200
    21.2 +++ b/src/Pure/Thy/bibtex.ML	Sun May 24 21:11:23 2020 +0200
    21.3 @@ -20,7 +20,7 @@
    21.4  type message = string * Position.T;
    21.5  
    21.6  fun check_database pos0 database =
    21.7 -  Scala.method "isabelle.Bibtex.check_database_yxml" database
    21.8 +  \<^scala>\<open>check_bibtex_database\<close> database
    21.9    |> YXML.parse_body
   21.10    |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
   21.11    |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0));
    22.1 --- a/src/Pure/Tools/build.ML	Sun May 24 09:04:25 2020 +0200
    22.2 +++ b/src/Pure/Tools/build.ML	Sun May 24 21:11:23 2020 +0200
    22.3 @@ -132,7 +132,8 @@
    22.4  (* build session *)
    22.5  
    22.6  datatype args = Args of
    22.7 - {symbol_codes: (string * int) list,
    22.8 + {pide: bool,
    22.9 +  symbol_codes: (string * int) list,
   22.10    command_timings: Properties.T list,
   22.11    verbose: bool,
   22.12    browser_info: Path.T,
   22.13 @@ -150,7 +151,7 @@
   22.14    loaded_theories: string list,
   22.15    bibtex_entries: string list};
   22.16  
   22.17 -fun decode_args yxml =
   22.18 +fun decode_args pide yxml =
   22.19    let
   22.20      open XML.Decode;
   22.21      val position = Position.of_properties o properties;
   22.22 @@ -167,7 +168,7 @@
   22.23                    (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
   22.24        (YXML.parse_body yxml);
   22.25    in
   22.26 -    Args {symbol_codes = symbol_codes, command_timings = command_timings,
   22.27 +    Args {pide = pide, symbol_codes = symbol_codes, command_timings = command_timings,
   22.28        verbose = verbose, browser_info = Path.explode browser_info,
   22.29        document_files = map (apply2 Path.explode) document_files,
   22.30        graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
   22.31 @@ -177,15 +178,16 @@
   22.32        bibtex_entries = bibtex_entries}
   22.33    end;
   22.34  
   22.35 -fun build_session (Args {symbol_codes, command_timings, verbose, browser_info, document_files,
   22.36 +fun build_session (Args {pide, symbol_codes, command_timings, verbose, browser_info, document_files,
   22.37      graph_file, parent_name, chapter, session_name, master_dir, theories, session_positions,
   22.38      session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) =
   22.39    let
   22.40      val symbols = HTML.make_symbols symbol_codes;
   22.41  
   22.42      val _ =
   22.43 -      Resources.init_session_base
   22.44 -        {session_positions = session_positions,
   22.45 +      Resources.init_session
   22.46 +        {pide = pide,
   22.47 +         session_positions = session_positions,
   22.48           session_directories = session_directories,
   22.49           docs = doc_names,
   22.50           global_theories = global_theories,
   22.51 @@ -233,7 +235,7 @@
   22.52      val _ = SHA1.test_samples ();
   22.53      val _ = Options.load_default ();
   22.54      val _ = Isabelle_Process.init_options ();
   22.55 -    val args = decode_args (File.read (Path.explode args_file));
   22.56 +    val args = decode_args false (File.read (Path.explode args_file));
   22.57      val _ =
   22.58        Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
   22.59          build_session args
   22.60 @@ -245,25 +247,24 @@
   22.61  
   22.62  (* PIDE version *)
   22.63  
   22.64 -fun build_session_finished errs =
   22.65 -  XML.Encode.list XML.Encode.string errs
   22.66 -  |> Output.protocol_message Markup.build_session_finished;
   22.67 -
   22.68  val _ =
   22.69    Isabelle_Process.protocol_command "build_session"
   22.70      (fn [args_yxml] =>
   22.71          let
   22.72 -          val args = decode_args args_yxml;
   22.73 -          val errs =
   22.74 -            Future.interruptible_task (fn () => (build_session args; [])) () handle exn =>
   22.75 -              (Runtime.exn_message_list exn handle _ (*sic!*) =>
   22.76 -                (build_session_finished ["CRASHED"];
   22.77 -                  raise Isabelle_Process.EXIT 2));
   22.78 -          val _ = build_session_finished errs;
   22.79 +          val args = decode_args true args_yxml;
   22.80 +          fun exec e =
   22.81 +            if can Theory.get_pure () then
   22.82 +              Isabelle_Thread.fork
   22.83 +                {name = "build_session", stack_limit = Isabelle_Thread.stack_limit (),
   22.84 +                  interrupts = false} e
   22.85 +              |> ignore
   22.86 +            else e ();
   22.87          in
   22.88 -          if null errs
   22.89 -          then raise Isabelle_Process.STOP
   22.90 -          else raise Isabelle_Process.EXIT 1
   22.91 +          exec (fn () =>
   22.92 +            (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
   22.93 +              ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
   22.94 +          |> let open XML.Encode in pair int (list string) end
   22.95 +          |> Output.protocol_message Markup.build_session_finished)
   22.96          end
   22.97        | _ => raise Match);
   22.98  
    23.1 --- a/src/Pure/Tools/build.scala	Sun May 24 09:04:25 2020 +0200
    23.2 +++ b/src/Pure/Tools/build.scala	Sun May 24 21:11:23 2020 +0200
    23.3 @@ -216,7 +216,7 @@
    23.4            }
    23.5            else Nil
    23.6  
    23.7 -        if (options.bool("pide_build")) {
    23.8 +        if (options.bool("pide_session")) {
    23.9            val resources = new Resources(sessions_structure, deps(parent))
   23.10            val session = new Session(options, resources)
   23.11  
   23.12 @@ -234,15 +234,23 @@
   23.13  
   23.14                private def build_session_finished(msg: Prover.Protocol_Output): Boolean =
   23.15                {
   23.16 -                val errors =
   23.17 +                val (rc, errors) =
   23.18                    try {
   23.19 -                    for (err <- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text)))
   23.20 -                    yield {
   23.21 -                      val prt = Protocol_Message.expose_no_reports(err)
   23.22 -                      Pretty.string_of(prt, metric = Symbol.Metric)
   23.23 +                    val (rc, errs) =
   23.24 +                    {
   23.25 +                      import XML.Decode._
   23.26 +                      pair(int, list(x => x))(Symbol.decode_yxml(msg.text))
   23.27                      }
   23.28 +                    val errors =
   23.29 +                      for (err <- errs) yield {
   23.30 +                        val prt = Protocol_Message.expose_no_reports(err)
   23.31 +                        Pretty.string_of(prt, metric = Symbol.Metric)
   23.32 +                      }
   23.33 +                    (rc, errors)
   23.34                    }
   23.35 -                  catch { case ERROR(err) => List(err) }
   23.36 +                  catch { case ERROR(err) => (2, List(err)) }
   23.37 +
   23.38 +                session.protocol_command("Prover.stop", rc.toString)
   23.39                  build_session_errors.fulfill(errors)
   23.40                  true
   23.41                }
    24.1 --- a/src/Pure/library.scala	Sun May 24 09:04:25 2020 +0200
    24.2 +++ b/src/Pure/library.scala	Sun May 24 21:11:23 2020 +0200
    24.3 @@ -144,6 +144,9 @@
    24.4  
    24.5    def isolate_substring(s: String): String = new String(s.toCharArray)
    24.6  
    24.7 +  def strip_ansi_color(s: String): String =
    24.8 +    s.replaceAll("""\u001b\[\d+m""", "")
    24.9 +
   24.10  
   24.11    /* quote */
   24.12  
    25.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sun May 24 09:04:25 2020 +0200
    25.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun May 24 21:11:23 2020 +0200
    25.3 @@ -25,6 +25,12 @@
    25.4  
    25.5  object JEdit_Lib
    25.6  {
    25.7 +  /* jEdit directories */
    25.8 +
    25.9 +  def directories: List[JFile] =
   25.10 +    (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_))
   25.11 +
   25.12 +
   25.13    /* location within multi-screen environment */
   25.14  
   25.15    final case class Screen_Location(point: Point, bounds: Rectangle)
    26.1 --- a/src/Tools/jEdit/src/scala_console.scala	Sun May 24 09:04:25 2020 +0200
    26.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Sun May 24 21:11:23 2020 +0200
    26.3 @@ -10,26 +10,12 @@
    26.4  import isabelle._
    26.5  
    26.6  import console.{Console, ConsolePane, Shell, Output}
    26.7 -
    26.8 -import org.gjt.sp.jedit.{jEdit, JARClassLoader}
    26.9 -import org.gjt.sp.jedit.MiscUtilities
   26.10 -
   26.11 -import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
   26.12 -
   26.13 -import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
   26.14 -import scala.tools.nsc.interpreter.IMain
   26.15 -import scala.collection.mutable
   26.16 +import org.gjt.sp.jedit.JARClassLoader
   26.17 +import java.io.{OutputStream, Writer, PrintWriter}
   26.18  
   26.19  
   26.20  class Scala_Console extends Shell("Scala")
   26.21  {
   26.22 -  /* reconstructed jEdit/plugin classpath */
   26.23 -
   26.24 -  private def jar_dirs: List[JFile] =
   26.25 -    (proper_string(jEdit.getSettingsDirectory).toList :::
   26.26 -     proper_string(jEdit.getJEditHome).toList).map(new JFile(_))
   26.27 -
   26.28 -
   26.29    /* global state -- owned by GUI thread */
   26.30  
   26.31    @volatile private var interpreters = Map.empty[Console, Interpreter]
   26.32 @@ -113,12 +99,11 @@
   26.33      private val running = Synchronized[Option[Thread]](None)
   26.34      def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
   26.35  
   26.36 -    private val settings = Scala.compiler_settings(error = report_error, jar_dirs = jar_dirs)
   26.37 -
   26.38 -    private val interp = new IMain(settings, new PrintWriter(console_writer, true))
   26.39 -    {
   26.40 -      override def parentClassLoader = new JARClassLoader
   26.41 -    }
   26.42 +    private val interp =
   26.43 +      Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
   26.44 +        interpreter(
   26.45 +          print_writer = new PrintWriter(console_writer, true),
   26.46 +          class_loader = new JARClassLoader)
   26.47  
   26.48      val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
   26.49      {