# HG changeset patch
# User desharna
# Date 1665672349 -7200
# Node ID bed09d3ddc237992e060eef9a86557389e442405
# Parent  3158975d80e279700074e3bbb285ddabadcec80c# Parent  e381884c09d4f47e5b7d28c1dd43361fe82abd1c
merged

diff -r 3158975d80e2 -r bed09d3ddc23 Admin/Windows/Cygwin/isabelle/postinstall
--- a/Admin/Windows/Cygwin/isabelle/postinstall	Thu Oct 13 14:30:53 2022 +0200
+++ b/Admin/Windows/Cygwin/isabelle/postinstall	Thu Oct 13 16:45:49 2022 +0200
@@ -4,8 +4,7 @@
 
 bash /etc/postinstall/base-files-mketc.sh.done
 
-mkpasswd -l >/etc/passwd
-mkgroup -l >/etc/group
+mkpasswd -l -u "$USERNAME" -p "$(cygpath -u "$HOMEDRIVE$HOMEPATH\\..")" >/etc/passwd
 
 find -type d -exec setfacl -m default:user::rwx,default:group::r-x,default:other:r-x '{}' +
 find -type d -exec chmod 755 '{}' +
diff -r 3158975d80e2 -r bed09d3ddc23 Admin/components/main
--- a/Admin/components/main	Thu Oct 13 14:30:53 2022 +0200
+++ b/Admin/components/main	Thu Oct 13 16:45:49 2022 +0200
@@ -20,7 +20,7 @@
 nunchaku-0.5
 opam-2.0.7
 pdfjs-2.14.305
-polyml-test-15c840d48c9a
+polyml-test-bafe319bc3a6-1
 postgresql-42.5.0
 scala-3.2.0
 smbc-0.4.1
diff -r 3158975d80e2 -r bed09d3ddc23 Admin/polyml/README
--- a/Admin/polyml/README	Thu Oct 13 14:30:53 2022 +0200
+++ b/Admin/polyml/README	Thu Oct 13 16:45:49 2022 +0200
@@ -3,8 +3,8 @@
 
 This compilation of Poly/ML (https://www.polyml.org) is based on the
 source distribution from
-https://github.com/polyml/polyml/commit/39d96a2def90 (official release
-5.9 with minimal additions fixes-5.9).
+https://github.com/polyml/polyml/commit/bafe319bc3a6 (after official
+version 5.9).
 
 The Isabelle repository provides an administrative tool "isabelle
 build_polyml", which can be used in the polyml component directory as
@@ -55,4 +55,4 @@
 
 
         Makarius
-        26-Nov-2021
+        09-Oct-2022
diff -r 3158975d80e2 -r bed09d3ddc23 Admin/polyml/settings
--- a/Admin/polyml/settings	Thu Oct 13 14:30:53 2022 +0200
+++ b/Admin/polyml/settings	Thu Oct 13 16:45:49 2022 +0200
@@ -2,7 +2,17 @@
 
 POLYML_HOME="$COMPONENT"
 
-ML_PLATFORM="${ISABELLE_APPLE_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}}"
+if [ -n "$ISABELLE_APPLE_PLATFORM64" ]
+then
+  if grep "ML_system_apple.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
+  then
+    ML_PLATFORM="$ISABELLE_PLATFORM64"
+  else
+    ML_PLATFORM="$ISABELLE_APPLE_PLATFORM64"
+  fi
+else
+  ML_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
+fi
 
 if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
 then
diff -r 3158975d80e2 -r bed09d3ddc23 NEWS
--- a/NEWS	Thu Oct 13 14:30:53 2022 +0200
+++ b/NEWS	Thu Oct 13 16:45:49 2022 +0200
@@ -238,6 +238,10 @@
       total_on_trancl
       totalp_on_tranclp
 
+* Theory "HOL-Library.Signed_Division": class signed_division carries
+assumptions; use syntactic type classes signed_division and
+signed_modulo as alternatives.
+
 * New theory "HOL-Library.NList" of fixed length lists.
 
 * New Theory "HOL-Library.Code_Abstract_Char" implements characters by
@@ -448,6 +452,11 @@
 together. Potential INCOMPATIBILITY for existing
 $ISABELLE_HOME_USER/etc/settings.
 
+* The system option "ML_system_apple" controls the use of native
+Apple/ARM64 for Poly/ML: default "true". Like "ML_system_64" this only
+works when saved in "$ISABELLE_HOME_USER/etc/preferences" (e.g. after
+shutdown of Isabelle/jEdit).
+
 
 
 New in Isabelle2021-1 (December 2021)
diff -r 3158975d80e2 -r bed09d3ddc23 etc/options
--- a/etc/options	Thu Oct 13 14:30:53 2022 +0200
+++ b/etc/options	Thu Oct 13 16:45:49 2022 +0200
@@ -161,7 +161,10 @@
   -- "ML debugger instrumentation for newly compiled code"
 
 public option ML_system_64 : bool = false
-  -- "ML system for 64bit platform is used if possible (change requires restart)"
+  -- "prefer native 64bit platform (change requires restart)"
+
+public option ML_system_apple : bool = true
+  -- "prefer native Apple/ARM64 platform (change requires restart)"
 
 public option ML_process_policy : string = ""
   -- "ML process command prefix (process policy)"
diff -r 3158975d80e2 -r bed09d3ddc23 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/Admin/build_release.scala	Thu Oct 13 16:45:49 2022 +0200
@@ -249,7 +249,8 @@
               "cd " + File.bash_path(remote_dir),
               "tar -xf tmp.tar",
               build_command,
-              """perl -pi -e "s/ISABELLE_APPLE_PLATFORM64/ISABELLE_WINDOWS_PLATFORM64/g;" "$(bin/isabelle getenv -b POLYML_HOME)/etc/settings" """,
+              """mkdir -p "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc" """,
+              """{ echo "ML_system_apple = false" > "$(bin/isabelle getenv -b ISABELLE_HOME_USER)/etc/preferences"; }""",
               build_command,
               "tar -cf tmp.tar heaps")
           ssh.execute(build_script.mkString(" && "), settings = false).check
diff -r 3158975d80e2 -r bed09d3ddc23 src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/General/bytes.ML	Thu Oct 13 16:45:49 2022 +0200
@@ -48,7 +48,7 @@
 
 (* primitive operations *)
 
-val chunk_size = 1024 * 1024 - 8;
+val chunk_size = 65000;
 
 abstype T = Bytes of
   {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)}
diff -r 3158975d80e2 -r bed09d3ddc23 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/General/http.scala	Thu Oct 13 16:45:49 2022 +0200
@@ -276,10 +276,11 @@
   }
 
   def server(
+    port: Int = 0,
     name: String = UUID.random().toString,
     services: List[Service] = isabelle_services
   ): Server = {
-    val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, 0), 0)
+    val http_server = HttpServer.create(new InetSocketAddress(isabelle.Server.localhost, port), 0)
     http_server.setExecutor(null)
 
     val server = new Server(name, http_server)
diff -r 3158975d80e2 -r bed09d3ddc23 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Oct 13 16:45:49 2022 +0200
@@ -99,7 +99,7 @@
   sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
 
-    def is_empty: Boolean = session_bases.isEmpty
+    def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty)
     def apply(name: String): Base = session_bases(name)
     def get(name: String): Option[Base] = session_bases.get(name)
 
diff -r 3158975d80e2 -r bed09d3ddc23 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Thu Oct 13 14:30:53 2022 +0200
+++ b/src/Pure/Tools/server_commands.scala	Thu Oct 13 16:45:49 2022 +0200
@@ -316,8 +316,8 @@
 
     override val command_body: Server.Command_Body =
       { case (context, Purge_Theories(args)) =>
-        val session = context.server.the_session(args.session_id)
-        command(args, session)._1
+          val session = context.server.the_session(args.session_id)
+          command(args, session)._1
       }
   }
 }