# HG changeset patch
# User paulson
# Date 1608824457 0
# Node ID ea0108cefc86643e5f512a4f47a7f00238639275
# Parent  a4efee8f88425e68103617a5f44ab1af9b9166f9# Parent  fc6597d50b4fbf32a7f140716ccf6d079d1780b2
merged

diff -r fc6597d50b4f -r ea0108cefc86 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Dec 24 13:10:18 2020 +0000
+++ b/Admin/components/components.sha1	Thu Dec 24 15:40:57 2020 +0000
@@ -321,6 +321,7 @@
 4d17611857fa3a93944c1f159c0fd2a161967aaf  sqlite-jdbc-3.27.2.1.tar.gz
 806be457eb79408fcc5a72aeca3f64b2d89a6b63  sqlite-jdbc-3.30.1.tar.gz
 cba2b194114216b226d75d49a70d1bd12b141ac8  sqlite-jdbc-3.32.3.2.tar.gz
+29306acd6ce9f4c87032b2c271c6df035fe7d4d3  sqlite-jdbc-3.34.0.tar.gz
 8d20968603f45a2c640081df1ace6a8b0527452a  sqlite-jdbc-3.8.11.2.tar.gz
 2369f06e8d095f9ba26df938b1a96000e535afff  ssh-java-20161009.tar.gz
 a2335d28b5b95d8d26500a53f1a9303fc5beaf36  ssh-java-20190323.tar.gz
diff -r fc6597d50b4f -r ea0108cefc86 Admin/components/main
--- a/Admin/components/main	Thu Dec 24 13:10:18 2020 +0000
+++ b/Admin/components/main	Thu Dec 24 15:40:57 2020 +0000
@@ -17,7 +17,7 @@
 scala-2.12.12
 smbc-0.4.1
 spass-3.8ds-2
-sqlite-jdbc-3.32.3.2
+sqlite-jdbc-3.34.0
 ssh-java-20190323
 stack-2.5.1
 vampire-4.2.2
diff -r fc6597d50b4f -r ea0108cefc86 lib/scripts/isabelle-platform
--- a/lib/scripts/isabelle-platform	Thu Dec 24 13:10:18 2020 +0000
+++ b/lib/scripts/isabelle-platform	Thu Dec 24 15:40:57 2020 +0000
@@ -6,6 +6,7 @@
 ISABELLE_PLATFORM_FAMILY=""
 ISABELLE_PLATFORM32=""
 ISABELLE_PLATFORM64=""
+ISABELLE_APPLE_PLATFORM64=""
 ISABELLE_WINDOWS_PLATFORM32=""
 ISABELLE_WINDOWS_PLATFORM64=""
 
@@ -34,6 +35,13 @@
         ;;
       *)
         ISABELLE_PLATFORM64=x86_64-darwin
+        case $(uname -m) in
+          arm64)
+            ISABELLE_APPLE_PLATFORM64=arm64-darwin
+            ;;
+          *)
+            ;;
+        esac
         ;;
     esac
     ;;
diff -r fc6597d50b4f -r ea0108cefc86 src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML	Thu Dec 24 13:10:18 2020 +0000
+++ b/src/HOL/Hoare/hoare_syntax.ML	Thu Dec 24 15:40:57 2020 +0000
@@ -206,11 +206,14 @@
 
 (** setup **)
 
+val _ =
+  Theory.setup
+   (Sign.parse_translation
+    [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
+     (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)]);
+
 fun setup consts =
   Data.put (SOME consts) #>
-  Sign.parse_translation
-   [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
-    (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)] #>
   Sign.print_translation
    [(#Valid consts, spec_tr' \<^syntax_const>\<open>_hoare\<close>),
     (#ValidTC consts, spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>)];
diff -r fc6597d50b4f -r ea0108cefc86 src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala	Thu Dec 24 13:10:18 2020 +0000
+++ b/src/Pure/Admin/build_sqlite.scala	Thu Dec 24 15:40:57 2020 +0000
@@ -67,6 +67,7 @@
           "META-INF/maven/org.xerial/sqlite-jdbc/LICENSE.zentus" -> ".",
           "org/sqlite/native/Linux/aarch64/libsqlitejdbc.so" -> "arm64-linux",
           "org/sqlite/native/Linux/x86_64/libsqlitejdbc.so" -> "x86_64-linux",
+          "org/sqlite/native/Mac/aarch64/libsqlitejdbc.jnilib" -> "arm64-darwin",
           "org/sqlite/native/Mac/x86_64/libsqlitejdbc.jnilib" -> "x86_64-darwin",
           "org/sqlite/native/Windows/x86_64/sqlitejdbc.dll" -> "x86_64-windows")
 
@@ -95,7 +96,8 @@
     -D DIR       target directory (default ".")
 
   Build sqlite-jdbc component from the specified download URL (JAR), see also
-  https://github.com/xerial/sqlite-jdbc/releases
+  https://github.com/xerial/sqlite-jdbc and
+  https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
 """,
         "D:" -> (arg => target_dir = Path.explode(arg)))
 
diff -r fc6597d50b4f -r ea0108cefc86 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Dec 24 13:10:18 2020 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Dec 24 15:40:57 2020 +0000
@@ -350,6 +350,7 @@
       List(
         Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
           options = "-m32 -M4" +
+            " -C /cygdrive/d/isatest/contrib" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
             " -e ISABELLE_GHC_SETUP=true" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
@@ -359,6 +360,7 @@
             Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")),
         Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
           options = "-m64 -M4" +
+            " -C /cygdrive/d/isatest/contrib" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
             " -e ISABELLE_GHC_SETUP=true" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",