# HG changeset patch # User wenzelm # Date 1612822496 -3600 # Node ID 180ecdf83bc8bdad17cb7b1fc184c6ccd1054bf2 # Parent b1aa641eee4c529497de1b43203903fa5793bed1# Parent 3d805ab66a2fbdbcac276356cd422b100dbec6f3 merged; diff -r b1aa641eee4c -r 180ecdf83bc8 .hgtags --- 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 diff -r b1aa641eee4c -r 180ecdf83bc8 ANNOUNCE --- 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: diff -r b1aa641eee4c -r 180ecdf83bc8 Admin/components/components.sha1 --- 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 diff -r b1aa641eee4c -r 180ecdf83bc8 Admin/components/main --- 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 diff -r b1aa641eee4c -r 180ecdf83bc8 NEWS --- 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). diff -r b1aa641eee4c -r 180ecdf83bc8 etc/settings --- 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 diff -r b1aa641eee4c -r 180ecdf83bc8 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 *) diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/ML/ml_system.ML --- 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 => diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/PIDE/protocol.ML --- 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; diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/PIDE/protocol_command.ML --- /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; diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/PIDE/resources.ML --- 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>\scala_function\ + (Scan.lift Parse.embedded_position) check_scala_function #> + ML_Antiquotation.inline_embedded \<^binding>\scala_function\ + (Args.context -- Scan.lift Parse.embedded_position + >> (uncurry check_scala_function #> ML_Syntax.print_string)) #> + ML_Antiquotation.value_embedded \<^binding>\scala\ + (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => + let val name = check_scala_function ctxt arg + in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #> + ML_Antiquotation.value_embedded \<^binding>\scala_thread\ + (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 *) diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/ROOT.ML --- 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" - diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/System/bash.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 \ 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; \ \ No newline at end of file diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/System/bash.scala --- 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)) + } + } } diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/System/isabelle_process.ML --- 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); diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/System/isabelle_system.scala --- 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 */ diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/System/kill.ML --- /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 +\ +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; +\ +else ML +\ +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; +\ diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/System/scala.ML --- 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>\scala_function\ - (Scan.lift Parse.embedded_position) check_function #> - ML_Antiquotation.inline_embedded \<^binding>\scala_function\ - (Args.context -- Scan.lift Parse.embedded_position - >> (uncurry check_function #> ML_Syntax.print_string)) #> - ML_Antiquotation.value_embedded \<^binding>\scala\ - (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => - let val name = check_function ctxt arg - in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end)) #> - ML_Antiquotation.value_embedded \<^binding>\scala_thread\ - (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; diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/System/scala.scala --- 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) diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/Tools/build.ML --- 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; diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/Tools/debugger.ML --- 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; diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/Tools/print_operation.ML --- 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 diff -r b1aa641eee4c -r 180ecdf83bc8 src/Pure/Tools/simplifier_trace.ML --- 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 diff -r b1aa641eee4c -r 180ecdf83bc8 src/Tools/jEdit/patches/laf_fonts --- /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 diff -r b1aa641eee4c -r 180ecdf83bc8 src/Tools/jEdit/src/jedit_editor.scala --- 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))