--- 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))