merged;
authorwenzelm
Mon, 08 Feb 2021 23:14:56 +0100
changeset 73484 180ecdf83bc8
parent 73467 b1aa641eee4c (current diff)
parent 73483 3d805ab66a2f (diff)
child 73485 27dc8f899147
child 74528 d605815cb4b9
merged;
--- a/.hgtags	Mon Feb 08 19:48:45 2021 +0100
+++ b/.hgtags	Mon Feb 08 23:14:56 2021 +0100
@@ -42,3 +42,4 @@
 802647edfe7be4478ca47a6e54e4d73733347e02 Isabelle2021-RC2
 02422c9add5e1c608290e48f3f0815c93ab00c1d Isabelle2021-RC3
 2ab14dbc6feb5e64c9c0c93ff2dff28f34a23f28 Isabelle2021-RC4
+a88dbf2a020fbd4ebee247f56fcc56e851e1f928 Isabelle2021-RC5
--- a/ANNOUNCE	Mon Feb 08 19:48:45 2021 +0100
+++ b/ANNOUNCE	Mon Feb 08 23:14:56 2021 +0100
@@ -28,7 +28,7 @@
 
 * System: support for Isabelle/Scala services defined in user-space.
 
-* Partial support for ARM64 platform on Linux and macOS (Apple Silicon).
+* Support for macOS Big Sur on Intel and Apple Silicon (ARM).
 
 
 You may get Isabelle2021 from the following mirror sites:
--- a/Admin/components/components.sha1	Mon Feb 08 19:48:45 2021 +0100
+++ b/Admin/components/components.sha1	Mon Feb 08 23:14:56 2021 +0100
@@ -84,6 +84,8 @@
 7a4b46752aa60c1ee6c53a2c128dedc8255a4568  flatlaf-0.46-1.tar.gz
 ed5cbc216389b655dac21a19e770a02a96867b85  flatlaf-0.46.tar.gz
 d37b38b9a27a6541c644e22eeebe9a339282173d  flatlaf-1.0-rc1.tar.gz
+dac46ce81cee10fb36a9d39b414dec7b7b671545  flatlaf-1.0-rc2.tar.gz
+d94e6da7299004890c04a7b395a3f2d381a3281e  flatlaf-1.0-rc3.tar.gz
 683acd94761ef460cca1a628f650355370de5afb  hol-light-bundle-0.5-126.tar.gz
 20b53cfc3ffc5b15c1eabc91846915b49b4c0367  isabelle_fonts-20151021.tar.gz
 736844204b2ef83974cd9f0a215738b767958c41  isabelle_fonts-20151104.tar.gz
@@ -191,6 +193,7 @@
 1c753beb93e92e95e99e8ead23a68346bd1af44a  jedit_build-20200610.tar.gz
 533b1ee6459f59bcbe4f09e214ad2cb990fb6952  jedit_build-20200908.tar.gz
 f9966b5ed26740bb5b8bddbfe947fcefaea43d4d  jedit_build-20201223.tar.gz
+0bdbd36eda5992396e9c6b66aa24259d4dd7559c  jedit_build-20210201.tar.gz
 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa  jfreechart-1.0.14-1.tar.gz
 8122526f1fc362ddae1a328bdbc2152853186fee  jfreechart-1.0.14.tar.gz
 d911f63a5c9b4c7335bb73f805cb1711ce017a84  jfreechart-1.5.0.tar.gz
@@ -218,6 +221,7 @@
 edcb517b7578db4eec1b6573b624f291776e11f6  naproche-20210124.tar.gz
 d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300  naproche-20210129.tar.gz
 810ee0f35adada9bf970c33fd80b986ab2255bf3  naproche-20210201.tar.gz
+e1b34e8f54e7e5844873612635444fed434718a1  naproche-7d0947a91dd5.tar.gz
 26df569cee9c2fd91b9ac06714afd43f3b37a1dd  nunchaku-0.3.tar.gz
 e573f2cbb57eb7b813ed5908753cfe2cb41033ca  nunchaku-0.5.tar.gz
 fe57793aca175336deea4f5e9c0d949a197850ac  opam-1.2.2.tar.gz
--- a/Admin/components/main	Mon Feb 08 19:48:45 2021 +0100
+++ b/Admin/components/main	Mon Feb 08 23:14:56 2021 +0100
@@ -4,10 +4,10 @@
 csdp-6.1.1
 cvc4-1.8
 e-2.5-1
-flatlaf-1.0-rc1
+flatlaf-1.0-rc3
 isabelle_fonts-20190717
 jdk-15.0.2+7
-jedit_build-20201223
+jedit_build-20210201
 jfreechart-1.5.1
 jortho-1.0-2
 kodkodi-1.5.6
--- a/NEWS	Mon Feb 08 19:48:45 2021 +0100
+++ b/NEWS	Mon Feb 08 23:14:56 2021 +0100
@@ -73,6 +73,9 @@
 Documents. See also $NAPROCHE_HOME/examples for files with .ftl or
 .ftl.tex extension.
 
+* Hyperlinks to various file-formats (.pdf, .png, etc.) open an external
+viewer, instead of re-using the jEdit text editor.
+
 
 *** Document preparation ***
 
@@ -373,9 +376,9 @@
 * Experimental support for arm64-linux platform. The reference platform
 is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
 
-* Partial support for arm64-darwin (Apple Silicon): most x86_64
-executables work well with runtime translation by Rosetta, but
-occasional problems remain (e.g. external provers).
+* Support for Apple Silicon, using mostly x86_64-darwin runtime
+translation via Rosetta 2 (e.g. Poly/ML and external provers), but also
+some native arm64-darwin executables (e.g. Java).
 
 
 
--- a/etc/settings	Mon Feb 08 19:48:45 2021 +0100
+++ b/etc/settings	Mon Feb 08 23:14:56 2021 +0100
@@ -112,7 +112,7 @@
 
 
 ###
-### Docs
+### Docs and external files
 ###
 
 # Where to look for docs (multiple dirs separated by ':').
@@ -136,6 +136,8 @@
 
 PDF_VIEWER="$ISABELLE_OPEN"
 
+ISABELLE_EXTERNAL_FILES="bmp:eps:gif:jpeg:jpg:pdf:png:xmp"
+
 
 ###
 ### Symbol rendering
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -865,10 +865,7 @@
         (l :: r :: []) => parse_term (unprefix " " r)
       | _ => raise Fail "unexpected equation in prolog output")
     fun parse_solution s = map dest_eq (space_explode ";" s)
-    val sols = (case space_explode "\n" sol of [] => [] | s => fst (split_last s))
-  in
-    map parse_solution sols
-  end
+  in map parse_solution (Library.trim_split_lines sol) end
 
 
 (* calling external interpreter and getting results *)
--- a/src/Pure/ML/ml_system.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/ML/ml_system.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -11,6 +11,7 @@
   val platform_is_windows: bool
   val platform_is_64: bool
   val platform_is_arm: bool
+  val platform_is_rosetta: unit -> bool
   val platform_path: string -> string
   val standard_path: string -> string
 end;
@@ -24,6 +25,12 @@
 val platform_is_64 = String.isPrefix "x86_64-" platform;
 val platform_is_arm = String.isPrefix "arm64-" platform;
 
+fun platform_is_rosetta () =
+  (case OS.Process.getEnv "ISABELLE_APPLE_PLATFORM64" of
+    NONE => false
+  | SOME "" => false
+  | SOME apple_platform => apple_platform <> platform);
+
 val platform_path =
   if platform_is_windows then
     fn path =>
--- a/src/Pure/PIDE/protocol.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/PIDE/protocol.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -8,27 +8,27 @@
 struct
 
 val _ =
-  Isabelle_Process.protocol_command "Prover.echo"
+  Protocol_Command.define "Prover.echo"
     (fn args => List.app writeln args);
 
 val _ =
-  Isabelle_Process.protocol_command "Prover.stop"
+  Protocol_Command.define "Prover.stop"
     (fn rc :: msgs =>
       (List.app Output.system_message msgs;
-       raise Isabelle_Process.STOP (Value.parse_int rc)));
+       raise Protocol_Command.STOP (Value.parse_int rc)));
 
 val _ =
-  Isabelle_Process.protocol_command "Prover.options"
+  Protocol_Command.define "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"
+  Protocol_Command.define "Prover.init_session"
     (fn [yxml] => Resources.init_session_yxml yxml);
 
 val _ =
-  Isabelle_Process.protocol_command "Document.define_blob"
+  Protocol_Command.define "Document.define_blob"
     (fn [digest, content] => Document.change_state (Document.define_blob digest content));
 
 fun decode_command id name parents_xml blobs_xml toks_xml sources : Document.command =
@@ -63,7 +63,7 @@
   Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)];
 
 val _ =
-  Isabelle_Process.protocol_command "Document.define_command"
+  Protocol_Command.define "Document.define_command"
     (fn id :: name :: parents :: blobs :: toks :: sources =>
       let
         val command =
@@ -73,7 +73,7 @@
       in commands_accepted [id] end);
 
 val _ =
-  Isabelle_Process.protocol_command "Document.define_commands"
+  Protocol_Command.define "Document.define_commands"
     (fn args =>
       let
         fun decode arg =
@@ -89,15 +89,15 @@
       in commands_accepted (map (Value.print_int o #command_id) commands) end);
 
 val _ =
-  Isabelle_Process.protocol_command "Document.discontinue_execution"
+  Protocol_Command.define "Document.discontinue_execution"
     (fn [] => Execution.discontinue ());
 
 val _ =
-  Isabelle_Process.protocol_command "Document.cancel_exec"
+  Protocol_Command.define "Document.cancel_exec"
     (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id));
 
 val _ =
-  Isabelle_Process.protocol_command "Document.update"
+  Protocol_Command.define "Document.update"
     (Future.task_context "Document.update" (Future.new_group NONE)
       (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml =>
         Document.change_state (fn state =>
@@ -150,7 +150,7 @@
           in Document.start_execution state' end)));
 
 val _ =
-  Isabelle_Process.protocol_command "Document.remove_versions"
+  Protocol_Command.define "Document.remove_versions"
     (fn [versions_yxml] => Document.change_state (fn state =>
       let
         val versions =
@@ -161,17 +161,17 @@
       in state1 end));
 
 val _ =
-  Isabelle_Process.protocol_command "Document.dialog_result"
+  Protocol_Command.define "Document.dialog_result"
     (fn [serial, result] =>
       Active.dialog_result (Value.parse_int serial) result
         handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
 
 val _ =
-  Isabelle_Process.protocol_command "ML_Heap.full_gc"
+  Protocol_Command.define "ML_Heap.full_gc"
     (fn [] => ML_Heap.full_gc ());
 
 val _ =
-  Isabelle_Process.protocol_command "ML_Heap.share_common_data"
+  Protocol_Command.define "ML_Heap.share_common_data"
     (fn [] => ML_Heap.share_common_data ());
 
 end;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/protocol_command.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -0,0 +1,47 @@
+(*  Title:      Pure/PIDE/protocol_command.ML
+    Author:     Makarius
+
+Protocol commands.
+*)
+
+signature PROTOCOL_COMMAND =
+sig
+  exception STOP of int
+  val is_protocol_exn: exn -> bool
+  val define: string -> (string list -> unit) -> unit
+  val run: string -> string list -> unit
+end;
+
+structure Protocol_Command: PROTOCOL_COMMAND =
+struct
+
+exception STOP of int;
+
+val is_protocol_exn = fn STOP _ => true | _ => false;
+
+local
+
+val commands =
+  Synchronized.var "Protocol_Command.commands"
+    (Symtab.empty: (string list -> unit) Symtab.table);
+
+in
+
+fun define name cmd =
+  Synchronized.change commands (fn cmds =>
+   (if not (Symtab.defined cmds name) then ()
+    else warning ("Redefining Isabelle protocol command " ^ quote name);
+    Symtab.update (name, cmd) cmds));
+
+fun run name args =
+  (case Symtab.lookup (Synchronized.value commands) name of
+    NONE => error ("Undefined Isabelle protocol command " ^ quote name)
+  | SOME cmd =>
+      (Runtime.exn_trace_system (fn () => cmd args)
+        handle exn =>
+          if is_protocol_exn exn then Exn.reraise exn
+          else error ("Isabelle protocol command failure: " ^ quote name)));
+
+end;
+
+end;
--- a/src/Pure/PIDE/resources.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/PIDE/resources.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -24,7 +24,8 @@
   val check_session: Proof.context -> string * Position.T -> string
   val session_chapter: string -> string
   val last_timing: Toplevel.transition -> Time.time
-  val scala_function_pos: string -> Position.T
+  val scala_functions: unit -> string list
+  val check_scala_function: Proof.context -> string * Position.T -> string
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -175,9 +176,34 @@
 
 fun last_timing tr = get_timings (get_session_base1 #timings) tr;
 
+
+(* Scala functions *)
+
+(*raw bootstrap environment*)
+fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
+
+(*regular resources*)
 fun scala_function_pos name =
-  Symtab.lookup (get_session_base1 #scala_functions) name
-  |> the_default Position.none;
+  (name, the_default Position.none (Symtab.lookup (get_session_base1 #scala_functions) name));
+
+fun check_scala_function ctxt arg =
+  Completion.check_entity Markup.scala_functionN
+    (scala_functions () |> sort_strings |> map scala_function_pos) ctxt arg;
+
+val _ = Theory.setup
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
+    (Scan.lift Parse.embedded_position) check_scala_function #>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
+    (Args.context -- Scan.lift Parse.embedded_position
+      >> (uncurry check_scala_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_scala_function ctxt arg
+      in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #>
+  ML_Antiquotation.value_embedded \<^binding>\<open>scala_thread\<close>
+    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+      let val name = check_scala_function ctxt arg
+      in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end)));
 
 
 (* manage source files *)
--- a/src/Pure/ROOT.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/ROOT.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -292,6 +292,9 @@
 ML_file "Proof/extraction.ML";
 
 (*Isabelle system*)
+ML_file "PIDE/protocol_command.ML";
+ML_file "System/scala.ML";
+ML_file "System/kill.ML";
 ML_file "System/bash.ML";
 ML_file "System/isabelle_system.ML";
 
@@ -324,7 +327,6 @@
 ML_file "System/command_line.ML";
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
-ML_file "System/scala.ML";
 ML_file "System/scala_compiler.ML";
 ML_file "System/isabelle_tool.ML";
 ML_file "Thy/bibtex.ML";
@@ -354,4 +356,3 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML"
-
--- a/src/Pure/System/bash.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/System/bash.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -11,11 +11,33 @@
   val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
 end;
 
+structure Bash: sig val terminate: int option -> unit end =
+struct
+
+fun terminate NONE = ()
+  | terminate (SOME pid) =
+      let
+        val kill = Kill.kill_group pid;
+
+        fun multi_kill count s =
+          count = 0 orelse
+            (kill s; kill Kill.SIGNONE) andalso
+            (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+        val _ =
+          multi_kill 7 Kill.SIGINT andalso
+          multi_kill 3 Kill.SIGTERM andalso
+          multi_kill 1 Kill.SIGKILL;
+      in () end;
+
+end;
+
 if ML_System.platform_is_windows then ML
 \<open>
 structure Bash: BASH =
 struct
 
+open Bash;
+
 val string = Bash_Syntax.string;
 val strings = Bash_Syntax.strings;
 
@@ -63,28 +85,6 @@
             NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
           | some => some);
 
-    fun terminate NONE = ()
-      | terminate (SOME pid) =
-          let
-            fun kill s =
-              let
-                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
-                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
-              in
-                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
-                  handle OS.SysErr _ => false
-              end;
-
-            fun multi_kill count s =
-              count = 0 orelse
-                (kill s; kill "0") andalso
-                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
-            val _ =
-              multi_kill 10 "INT" andalso
-              multi_kill 10 "TERM" andalso
-              multi_kill 10 "KILL";
-          in () end;
-
     fun cleanup () =
      (Isabelle_Thread.interrupt_unsynchronized system_thread;
       cleanup_files ());
@@ -110,10 +110,12 @@
 structure Bash: BASH =
 struct
 
+open Bash;
+
 val string = Bash_Syntax.string;
 val strings = Bash_Syntax.strings;
 
-val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
+val process_ml = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
   let
     datatype result = Wait | Signal | Result of int;
     val result = Synchronized.var "bash_result" Wait;
@@ -163,24 +165,6 @@
             NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
           | some => some);
 
-    fun terminate NONE = ()
-      | terminate (SOME pid) =
-          let
-            fun kill s =
-              (Posix.Process.kill
-                (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
-              handle OS.SysErr _ => false;
-
-            fun multi_kill count s =
-              count = 0 orelse
-                (kill s; kill (Posix.Signal.fromWord 0w0)) andalso
-                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
-            val _ =
-              multi_kill 10 Posix.Signal.int andalso
-              multi_kill 10 Posix.Signal.term andalso
-              multi_kill 10 Posix.Signal.kill;
-          in () end;
-
     fun cleanup () =
      (Isabelle_Thread.interrupt_unsynchronized system_thread;
       cleanup_files ());
@@ -199,5 +183,25 @@
     handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   end);
 
+fun process_scala script =
+  Scala.function "bash_process"
+    ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script)
+  |> YXML.parse_body
+  |>
+    let open XML.Decode in
+      variant
+       [fn ([], []) => raise Exn.Interrupt,
+        fn ([], a) => error (YXML.string_of_body a),
+        fn ([a, b], c) =>
+          let
+            val rc = int_atom a;
+            val pid = int_atom b;
+            val (out, err) = pair I I c |> apply2 YXML.string_of_body;
+          in {out = out, err = err, rc = rc, terminate = fn () => terminate (SOME pid)} end]
+    end;
+
+fun process script =
+  if ML_System.platform_is_rosetta () then process_scala script else process_ml script;
+
 end;
 \<close>
\ No newline at end of file
--- a/src/Pure/System/bash.scala	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/System/bash.scala	Mon Feb 08 23:14:56 2021 +0100
@@ -202,4 +202,41 @@
       Process_Result(rc, out_lines.join, err_lines.join, get_timing)
     }
   }
+
+
+  /* Scala function */
+
+  object Process extends Scala.Fun("bash_process")
+  {
+    val here = Scala_Project.here
+    def apply(script: String): String =
+    {
+      val result =
+        Exn.capture {
+          val proc = process(script)
+          val res = proc.result()
+          (res, proc.pid)
+        }
+
+      val is_interrupt =
+        result match {
+          case Exn.Res((res, _)) => res.rc == Exn.Interrupt.return_code
+          case Exn.Exn(exn) => Exn.is_interrupt(exn)
+        }
+
+      val encode: XML.Encode.T[Exn.Result[(Process_Result, String)]] =
+      {
+        import XML.Encode._
+        val string = XML.Encode.string
+        variant(List(
+          { case _ if is_interrupt => (Nil, Nil) },
+          { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) },
+          { case Exn.Res((res, pid)) =>
+              val out = Library.terminate_lines(res.out_lines)
+              val err = Library.terminate_lines(res.err_lines)
+              (List(int_atom(res.rc), pid), pair(string, string)(out, err)) }))
+      }
+      YXML.string_of_body(encode(result))
+    }
+  }
 }
--- a/src/Pure/System/isabelle_process.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/System/isabelle_process.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -7,8 +7,6 @@
 signature ISABELLE_PROCESS =
 sig
   val is_active: unit -> bool
-  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
   val init_options: unit -> unit
@@ -33,38 +31,6 @@
 val protocol_modes2 = [isabelle_processN, Pretty.symbolicN];
 
 
-(* protocol commands *)
-
-exception STOP of int;
-
-val is_protocol_exn = fn STOP _ => true | _ => false;
-
-local
-
-val commands =
-  Synchronized.var "Isabelle_Process.commands"
-    (Symtab.empty: (string list -> unit) Symtab.table);
-
-in
-
-fun protocol_command name cmd =
-  Synchronized.change commands (fn cmds =>
-   (if not (Symtab.defined cmds name) then ()
-    else warning ("Redefining Isabelle protocol command " ^ quote name);
-    Symtab.update (name, cmd) cmds));
-
-fun run_command name args =
-  (case Symtab.lookup (Synchronized.value commands) name of
-    NONE => error ("Undefined Isabelle protocol command " ^ quote name)
-  | SOME cmd =>
-      (Runtime.exn_trace_system (fn () => cmd args)
-        handle exn =>
-          if is_protocol_exn exn then Exn.reraise exn
-          else error ("Isabelle protocol command failure: " ^ quote name)));
-
-end;
-
-
 (* restricted tracing messages *)
 
 val tracing_messages =
@@ -192,11 +158,11 @@
       let
         val _ =
           (case Byte_Message.read_message in_stream of
-            NONE => raise STOP 0
+            NONE => raise Protocol_Command.STOP 0
           | SOME [] => Output.system_message "Isabelle process: no input"
-          | SOME (name :: args) => run_command name args)
+          | SOME (name :: args) => Protocol_Command.run name args)
           handle exn =>
-            if is_protocol_exn exn then Exn.reraise exn
+            if Protocol_Command.is_protocol_exn exn then Exn.reraise exn
             else (Runtime.exn_system_message exn handle crash => recover crash);
       in protocol_loop () end;
 
@@ -219,7 +185,7 @@
     val _ = Options.reset_default ();
   in
     (case result of
-      Exn.Exn (STOP rc) => if rc = 0 then () else exit rc
+      Exn.Exn (Protocol_Command.STOP rc) => if rc = 0 then () else exit rc
     | _ => Exn.release result)
   end);
 
--- a/src/Pure/System/isabelle_system.scala	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Mon Feb 08 23:14:56 2021 +0100
@@ -404,12 +404,24 @@
   def pdf_viewer(arg: Path): Unit =
     bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
 
+  def open_external_file(name: String): Boolean =
+  {
+    val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
+    val external =
+      ext.nonEmpty &&
+      Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
+    if (external) {
+      if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
+      else open(name)
+    }
+    external
+  }
+
   def export_isabelle_identifier(isabelle_identifier: String): String =
     if (isabelle_identifier == "") ""
     else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
 
 
-
   /** Isabelle resources **/
 
   /* repository clone with Admin */
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/kill.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -0,0 +1,59 @@
+(*  Title:      Pure/System/kill.ML
+    Author:     Makarius
+
+Kill external process group.
+*)
+
+signature KILL =
+sig
+  type signal
+  val SIGNONE: signal
+  val SIGINT: signal
+  val SIGTERM: signal
+  val SIGKILL: signal
+  val kill_group: int -> signal -> bool
+end;
+
+if ML_System.platform_is_windows then ML
+\<open>
+structure Kill: KILL =
+struct
+
+type signal = string;
+
+val SIGNONE = "0";
+val SIGINT = "INT";
+val SIGTERM = "TERM";
+val SIGKILL = "KILL";
+
+fun kill_group pid s =
+  let
+    val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
+    val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
+  in
+    OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
+      handle OS.SysErr _ => false
+  end;
+
+end;
+\<close>
+else ML
+\<open>
+structure Kill: KILL =
+struct
+
+type signal = Posix.Signal.signal;
+
+val SIGNONE = Posix.Signal.fromWord 0w0;
+val SIGINT = Posix.Signal.int;
+val SIGTERM = Posix.Signal.term;
+val SIGKILL = Posix.Signal.kill;
+
+fun kill_group pid s =
+  let
+    val arg = Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid));
+    val _ = Posix.Process.kill (arg, s);
+  in true end handle OS.SysErr _ => false;
+
+end;
+\<close>
--- a/src/Pure/System/scala.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/System/scala.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/System/scala.ML
     Author:     Makarius
 
-Support for Scala at runtime.
+Invoke Scala functions from the ML runtime.
 *)
 
 signature SCALA =
@@ -9,15 +9,11 @@
   exception Null
   val function: string -> string -> string
   val function_thread: string -> string -> string
-  val functions: unit -> string list
-  val check_function: Proof.context -> string * Position.T -> string
 end;
 
 structure Scala: SCALA =
 struct
 
-(** protocol for Scala function invocation from ML **)
-
 exception Null;
 
 local
@@ -28,7 +24,7 @@
   Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table);
 
 val _ =
-  Isabelle_Process.protocol_command "Scala.result"
+  Protocol_Command.define "Scala.result"
     (fn [id, tag, res] =>
       let
         val result =
@@ -71,29 +67,4 @@
 
 end;
 
-
-
-(** registered Scala functions **)
-
-fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
-
-fun check_function ctxt arg =
-  Completion.check_entity Markup.scala_functionN
-    (functions () |> sort_strings |> map (fn a => (a, Resources.scala_function_pos a))) ctxt arg;
-
-val _ = Theory.setup
- (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<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)) #>
-  ML_Antiquotation.value_embedded \<^binding>\<open>scala_thread\<close>
-    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
-      let val name = check_function ctxt arg
-      in ML_Syntax.atomic ("Scala.function_thread " ^ ML_Syntax.print_string name) end)));
-
 end;
--- a/src/Pure/System/scala.scala	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/System/scala.scala	Mon Feb 08 23:14:56 2021 +0100
@@ -243,5 +243,6 @@
   Scala.Sleep,
   Scala.Toplevel,
   Doc.Doc_Names,
+  Bash.Process,
   Bibtex.Check_Database,
   Isabelle_Tool.Isabelle_Tools)
--- a/src/Pure/Tools/build.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/Tools/build.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -50,7 +50,7 @@
 (* build session *)
 
 val _ =
-  Isabelle_Process.protocol_command "build_session"
+  Protocol_Command.define "build_session"
     (fn [resources_yxml, args_yxml] =>
         let
           val _ = Resources.init_session_yxml resources_yxml;
--- a/src/Pure/Tools/debugger.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/Tools/debugger.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -243,7 +243,7 @@
 (** protocol commands **)
 
 val _ =
-  Isabelle_Process.protocol_command "Debugger.init"
+  Protocol_Command.define "Debugger.init"
     (fn [] =>
      (init_input ();
       PolyML.DebuggerInterface.setOnBreakPoint
@@ -256,15 +256,15 @@
           else ()))));
 
 val _ =
-  Isabelle_Process.protocol_command "Debugger.exit"
+  Protocol_Command.define "Debugger.exit"
     (fn [] => (PolyML.DebuggerInterface.setOnBreakPoint NONE; exit_input ()));
 
 val _ =
-  Isabelle_Process.protocol_command "Debugger.break"
+  Protocol_Command.define "Debugger.break"
     (fn [b] => set_break (Value.parse_bool b));
 
 val _ =
-  Isabelle_Process.protocol_command "Debugger.breakpoint"
+  Protocol_Command.define "Debugger.breakpoint"
     (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
       let
         val id = Value.parse_int id0;
@@ -289,7 +289,7 @@
       end);
 
 val _ =
-  Isabelle_Process.protocol_command "Debugger.input"
+  Protocol_Command.define "Debugger.input"
     (fn thread_name :: msg => input thread_name msg);
 
 end;
--- a/src/Pure/Tools/print_operation.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/Tools/print_operation.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -27,7 +27,7 @@
       |> map (fn (x, (y, _)) => (x, y)) |> rev
       |> let open XML.Encode in list (pair string string) end);
 
-val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
+val _ = Protocol_Command.define "print_operations" (fn [] => report ());
 
 in
 
--- a/src/Pure/Tools/simplifier_trace.ML	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML	Mon Feb 08 23:14:56 2021 +0100
@@ -400,7 +400,7 @@
      trace_apply = simp_apply})
 
 val _ =
-  Isabelle_Process.protocol_command "Simplifier_Trace.reply"
+  Protocol_Command.define "Simplifier_Trace.reply"
     (fn [serial_string, reply] =>
       let
         val serial = Value.parse_int serial_string
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/laf_fonts	Mon Feb 08 23:14:56 2021 +0100
@@ -0,0 +1,13 @@
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2020-09-03 05:31:04.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2021-02-01 18:00:07.541681144 +0100
+@@ -414,7 +414,9 @@
+ 
+ 		// adjust swing properties for button, menu, and label, and list and
+ 		// textfield fonts
+-		setFonts();
++		if (!jEdit.getProperty("lookAndFeel").startsWith("com.formdev.flatlaf.")) {
++			setFonts();
++		}
+ 
+ 		// This is handled a little differently from other jEdit settings
+ 		// as this flag needs to be known very early in the
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Feb 08 19:48:45 2021 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Feb 08 23:14:56 2021 +0100
@@ -166,7 +166,7 @@
           catch { case ERROR(_) => false }
 
         if (is_dir) VFSBrowser.browseDirectory(view, name)
-        else {
+        else if (!Isabelle_System.open_external_file(name)) {
           val args =
             if (line <= 0) Array(name)
             else if (column <= 0) Array(name, "+line:" + (line + 1))