# HG changeset patch # User desharna # Date 1613374579 -3600 # Node ID efeebcfaef8594f079dd31bec93823fa011eb90d # Parent dcf295994c906b089556876ffd329d6dbdab245b# Parent 15ea7f6fb4220d5d24cbead8b85c155ef9fe68bf merged diff -r dcf295994c90 -r efeebcfaef85 .hgtags --- a/.hgtags Fri Feb 12 11:21:44 2021 +0100 +++ b/.hgtags Mon Feb 15 08:36:19 2021 +0100 @@ -43,3 +43,4 @@ 02422c9add5e1c608290e48f3f0815c93ab00c1d Isabelle2021-RC3 2ab14dbc6feb5e64c9c0c93ff2dff28f34a23f28 Isabelle2021-RC4 a88dbf2a020fbd4ebee247f56fcc56e851e1f928 Isabelle2021-RC5 +ed36e33a2e4b01751c93c8ad28c07f8b00e11722 Isabelle2021-RC6 diff -r dcf295994c90 -r efeebcfaef85 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Feb 12 11:21:44 2021 +0100 +++ b/Admin/components/components.sha1 Mon Feb 15 08:36:19 2021 +0100 @@ -86,6 +86,7 @@ d37b38b9a27a6541c644e22eeebe9a339282173d flatlaf-1.0-rc1.tar.gz dac46ce81cee10fb36a9d39b414dec7b7b671545 flatlaf-1.0-rc2.tar.gz d94e6da7299004890c04a7b395a3f2d381a3281e flatlaf-1.0-rc3.tar.gz +7ca3e6a8c9bd837990e64d89e7fa07a7e7cf78ff flatlaf-1.0.tar.gz 683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz 20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz 736844204b2ef83974cd9f0a215738b767958c41 isabelle_fonts-20151104.tar.gz @@ -221,6 +222,7 @@ edcb517b7578db4eec1b6573b624f291776e11f6 naproche-20210124.tar.gz d858eb0ede6aea6b8cc40de63bd3a17f8f9f5300 naproche-20210129.tar.gz 810ee0f35adada9bf970c33fd80b986ab2255bf3 naproche-20210201.tar.gz +77252e0b40f89825b9b5935f9f0c4cd5d4e7012a naproche-6d0d76ce2f2a.tar.gz e1b34e8f54e7e5844873612635444fed434718a1 naproche-7d0947a91dd5.tar.gz 26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz diff -r dcf295994c90 -r efeebcfaef85 Admin/components/main --- a/Admin/components/main Fri Feb 12 11:21:44 2021 +0100 +++ b/Admin/components/main Mon Feb 15 08:36:19 2021 +0100 @@ -4,7 +4,7 @@ csdp-6.1.1 cvc4-1.8 e-2.5-1 -flatlaf-1.0-rc3 +flatlaf-1.0 isabelle_fonts-20190717 jdk-15.0.2+7 jedit_build-20210201 diff -r dcf295994c90 -r efeebcfaef85 NEWS --- a/NEWS Fri Feb 12 11:21:44 2021 +0100 +++ b/NEWS Mon Feb 15 08:36:19 2021 +0100 @@ -69,12 +69,14 @@ * Improved GUI support for macOS 11.1 Big Sur: native fullscreen mode, but non-native look-and-feel (FlatLaf). +* Hyperlinks to various file-formats (.pdf, .png, etc.) open an external +viewer, instead of re-using the jEdit text editor. + * IDE support for Naproche-SAD: Proof Checking of Natural Mathematical 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. +.ftl.tex extension. The corresponding Naproche-SAD server process can be +disabled by setting the system option naproche_server=false and +restarting the Isabelle application. *** Document preparation *** diff -r dcf295994c90 -r efeebcfaef85 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Fri Feb 12 11:21:44 2021 +0100 +++ b/src/Pure/Admin/build_history.scala Mon Feb 15 08:36:19 2021 +0100 @@ -192,7 +192,7 @@ components_base = components_base, catalogs = List("main", "optional")) other_isabelle.init_settings(component_settings ::: init_settings) - other_isabelle.resolve_components(verbose) + other_isabelle.resolve_components(echo = verbose) val ml_platform = augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings) @@ -205,7 +205,7 @@ val isabelle_base_log = isabelle_output + Path.explode("../base_log") if (first_build) { - other_isabelle.resolve_components(verbose) + other_isabelle.resolve_components(echo = verbose) if (fresh) Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes")) diff -r dcf295994c90 -r efeebcfaef85 src/Pure/Admin/other_isabelle.scala --- a/src/Pure/Admin/other_isabelle.scala Fri Feb 12 11:21:44 2021 +0100 +++ b/src/Pure/Admin/other_isabelle.scala Mon Feb 15 08:36:19 2021 +0100 @@ -50,7 +50,9 @@ bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict) def resolve_components(echo: Boolean): Unit = - other_isabelle("components -a", redirect = true, echo = echo).check + other_isabelle( + "env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) + + " isabelle components -a", redirect = true, echo = echo).check def getenv(name: String): String = other_isabelle("getenv -b " + Bash.string(name)).check.out diff -r dcf295994c90 -r efeebcfaef85 src/Pure/System/bash.ML --- a/src/Pure/System/bash.ML Fri Feb 12 11:21:44 2021 +0100 +++ b/src/Pure/System/bash.ML Mon Feb 15 08:36:19 2021 +0100 @@ -184,7 +184,7 @@ end); fun process_scala script = - Scala.function "bash_process" + Scala.function_thread "bash_process" ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |> YXML.parse_body |> diff -r dcf295994c90 -r efeebcfaef85 src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML Fri Feb 12 11:21:44 2021 +0100 +++ b/src/Pure/System/scala.ML Mon Feb 15 08:36:19 2021 +0100 @@ -53,11 +53,11 @@ (case Symtab.lookup tab id of SOME (Exn.Exn Match) => NONE | SOME result => SOME (result, Symtab.delete id tab) - | NONE => SOME (Exn.Exn Exn.Interrupt, tab))) - handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn); + | NONE => SOME (Exn.Exn Exn.Interrupt, tab))); in invoke (); Exn.release (restore_attributes await_result ()) + handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn) end) (); in diff -r dcf295994c90 -r efeebcfaef85 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Fri Feb 12 11:21:44 2021 +0100 +++ b/src/Tools/Haskell/Haskell.thy Mon Feb 15 08:36:19 2021 +0100 @@ -167,7 +167,7 @@ \ generate_file "Isabelle/Value.hs" = \ -{- Title: Haskell/Tools/Value.hs +{- Title: Isabelle/Value.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) @@ -296,7 +296,7 @@ \ generate_file "Isabelle/Markup.hs" = \ -{- Title: Haskell/Tools/Markup.hs +{- Title: Isabelle/Markup.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle)