--- 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
--- 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
--- 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
--- 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 ***
--- 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"))
--- 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
--- 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
|>
--- 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
--- 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 @@
\<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)