# HG changeset patch # User wenzelm # Date 1613329993 -3600 # Node ID 15ea7f6fb4220d5d24cbead8b85c155ef9fe68bf # Parent 7f55a3e28c88f137d202cc4baba367c5f796253a# Parent e3e117660199e457c031c209809494307ef9dbb9 merged diff -r 7f55a3e28c88 -r 15ea7f6fb422 .hgtags --- a/.hgtags Fri Feb 12 12:13:24 2021 +0100 +++ b/.hgtags Sun Feb 14 20:13:13 2021 +0100 @@ -43,3 +43,4 @@ 02422c9add5e1c608290e48f3f0815c93ab00c1d Isabelle2021-RC3 2ab14dbc6feb5e64c9c0c93ff2dff28f34a23f28 Isabelle2021-RC4 a88dbf2a020fbd4ebee247f56fcc56e851e1f928 Isabelle2021-RC5 +ed36e33a2e4b01751c93c8ad28c07f8b00e11722 Isabelle2021-RC6 diff -r 7f55a3e28c88 -r 15ea7f6fb422 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Feb 12 12:13:24 2021 +0100 +++ b/Admin/components/components.sha1 Sun Feb 14 20:13:13 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 7f55a3e28c88 -r 15ea7f6fb422 Admin/components/main --- a/Admin/components/main Fri Feb 12 12:13:24 2021 +0100 +++ b/Admin/components/main Sun Feb 14 20:13:13 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 7f55a3e28c88 -r 15ea7f6fb422 NEWS --- a/NEWS Fri Feb 12 12:13:24 2021 +0100 +++ b/NEWS Sun Feb 14 20:13:13 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 7f55a3e28c88 -r 15ea7f6fb422 src/Pure/System/bash.ML --- a/src/Pure/System/bash.ML Fri Feb 12 12:13:24 2021 +0100 +++ b/src/Pure/System/bash.ML Sun Feb 14 20:13:13 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 7f55a3e28c88 -r 15ea7f6fb422 src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML Fri Feb 12 12:13:24 2021 +0100 +++ b/src/Pure/System/scala.ML Sun Feb 14 20:13:13 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 7f55a3e28c88 -r 15ea7f6fb422 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Fri Feb 12 12:13:24 2021 +0100 +++ b/src/Tools/Haskell/Haskell.thy Sun Feb 14 20:13:13 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)