merged
authorwenzelm
Sun, 14 Feb 2021 20:13:13 +0100
changeset 73251 15ea7f6fb422
parent 73243 7f55a3e28c88 (current diff)
parent 73250 e3e117660199 (diff)
child 73252 b4552595b04e
child 73291 efeebcfaef85
merged
--- 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
--- 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
--- 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
--- 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 ***
--- 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
   |>
--- 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
--- 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 @@
 \<close>
 
 generate_file "Isabelle/Value.hs" = \<open>
-{-  Title:      Haskell/Tools/Value.hs
+{-  Title:      Isabelle/Value.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)
 
@@ -296,7 +296,7 @@
 \<close>
 
 generate_file "Isabelle/Markup.hs" = \<open>
-{-  Title:      Haskell/Tools/Markup.hs
+{-  Title:      Isabelle/Markup.hs
     Author:     Makarius
     LICENSE:    BSD 3-clause (Isabelle)