# HG changeset patch
# User wenzelm
# Date 1476723793 -7200
# Node ID a65ff5a84296391d4e4816ab115a312e785eedc0
# Parent  2e94501cbc347bfe49ed799ae1bccddc229dd595# Parent  298a6df049f06f1b21625e25c28ac70fd77dc76f
merged

diff -r 2e94501cbc34 -r a65ff5a84296 NEWS
--- a/NEWS	Mon Oct 17 18:53:45 2016 +0200
+++ b/NEWS	Mon Oct 17 19:03:13 2016 +0200
@@ -992,6 +992,10 @@
 given heap image. Errors lead to premature exit of the ML process with
 return code 1.
 
+* The system option "threads" (for the size of the Isabelle/ML thread
+farm) is also passed to the underlying ML runtime system as --gcthreads,
+unless there is already a default provided via ML_OPTIONS settings.
+
 * Command-line tool "isabelle console" provides option -r to help to
 bootstrapping Isabelle/Pure interactively.
 
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Mon Oct 17 19:03:13 2016 +0200
@@ -103,8 +103,10 @@
 
   private val remote_builds =
     List(
-      Remote_Build("lxbroy10", options = "-m32 -M4", shared_home = true),
-      Remote_Build("macbroy2", options = "-m32 -M4"))
+      Remote_Build("lxbroy10", options = "-m32 -M4 -N", shared_home = true),
+      Remote_Build("macbroy2", options = "-m32 -M4"),
+      Remote_Build("macbroy30", options = "-m32 -M2"),
+      Remote_Build("macbroy31", options = "-m32 -M2"))
 
   private def remote_build_history(rev: String, r: Remote_Build): Logger_Task =
     Logger_Task("build_history-" + r.host, logger =>
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -123,10 +123,10 @@
 fun SYNCHRONIZED name = Multithreading.synchronized name lock;
 
 fun wait cond = (*requires SYNCHRONIZED*)
-  Multithreading.sync_wait NONE NONE cond lock;
+  Multithreading.sync_wait NONE cond lock;
 
 fun wait_timeout timeout cond = (*requires SYNCHRONIZED*)
-  Multithreading.sync_wait NONE (SOME (Time.now () + timeout)) cond lock;
+  Multithreading.sync_wait (SOME (Time.now () + timeout)) cond lock;
 
 fun signal cond = (*requires SYNCHRONIZED*)
   ConditionVar.signal cond;
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -9,8 +9,7 @@
   val max_threads: unit -> int
   val max_threads_update: int -> unit
   val enabled: unit -> bool
-  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
-    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
+  val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
@@ -47,10 +46,9 @@
 
 (* synchronous wait *)
 
-fun sync_wait opt_atts time cond lock =
+fun sync_wait time cond lock =
   Thread_Attributes.with_attributes
-    (Thread_Attributes.sync_interrupts
-      (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
+    (Thread_Attributes.sync_interrupts (Thread.getAttributes ()))
     (fn _ =>
       (case time of
         SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -37,7 +37,7 @@
       fun wait () =
         (case peek v of
           NONE =>
-            (case Multithreading.sync_wait NONE NONE cond lock of
+            (case Multithreading.sync_wait NONE cond lock of
               Exn.Res _ => wait ()
             | Exn.Exn exn => Exn.reraise exn)
         | SOME x => x);
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -46,7 +46,7 @@
         let val x = ! var in
           (case f x of
             NONE =>
-              (case Multithreading.sync_wait NONE (time_limit x) cond lock of
+              (case Multithreading.sync_wait (time_limit x) cond lock of
                 Exn.Res true => try_change ()
               | Exn.Res false => NONE
               | Exn.Exn exn => Exn.reraise exn)
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/General/sha1.ML
--- a/src/Pure/General/sha1.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/General/sha1.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -42,7 +42,7 @@
 fun hex_digit (text, w: Word32.word) =
   let
     val d = Word32.toInt (w andb 0wxf);
-    val dig = if d < 10 then chr (ord "0" + d) else chr (ord "a" + d - 10);
+    val dig = if d < 10 then chr (Char.ord #"0" + d) else chr (Char.ord #"a" + d - 10);
   in (dig ^ text, w >> 0w4) end;
 
 fun hex_word w = #1 (funpow 8 hex_digit ("", w));
@@ -145,7 +145,7 @@
 
 (* digesting *)
 
-fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
+fun hex_digit i = if i < 10 then chr (Char.ord #"0" + i) else chr (Char.ord #"a" + i - 10);
 
 fun hex_string arr i =
   let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/General/symbol.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -121,7 +121,7 @@
 val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
 
 fun is_printable s =
-  if is_char s then ord space <= ord s andalso ord s <= ord "~"
+  if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~"
   else is_utf8 s orelse raw_symbolic s;
 
 fun is_control s =
@@ -148,17 +148,17 @@
 
 fun is_ascii_letter s =
   is_char s andalso
-   (ord "A" <= ord s andalso ord s <= ord "Z" orelse
-    ord "a" <= ord s andalso ord s <= ord "z");
+   (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z" orelse
+    Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z");
 
 fun is_ascii_digit s =
-  is_char s andalso ord "0" <= ord s andalso ord s <= ord "9";
+  is_char s andalso Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9";
 
 fun is_ascii_hex s =
   is_char s andalso
-   (ord "0" <= ord s andalso ord s <= ord "9" orelse
-    ord "A" <= ord s andalso ord s <= ord "F" orelse
-    ord "a" <= ord s andalso ord s <= ord "f");
+   (Char.ord #"0" <= ord s andalso ord s <= Char.ord #"9" orelse
+    Char.ord #"A" <= ord s andalso ord s <= Char.ord #"F" orelse
+    Char.ord #"a" <= ord s andalso ord s <= Char.ord #"f");
 
 fun is_ascii_quasi "_" = true
   | is_ascii_quasi "'" = true
@@ -172,11 +172,11 @@
 
 fun is_ascii_letdig s = is_ascii_letter s orelse is_ascii_digit s orelse is_ascii_quasi s;
 
-fun is_ascii_lower s = is_char s andalso (ord "a" <= ord s andalso ord s <= ord "z");
-fun is_ascii_upper s = is_char s andalso (ord "A" <= ord s andalso ord s <= ord "Z");
+fun is_ascii_lower s = is_char s andalso (Char.ord #"a" <= ord s andalso ord s <= Char.ord #"z");
+fun is_ascii_upper s = is_char s andalso (Char.ord #"A" <= ord s andalso ord s <= Char.ord #"Z");
 
-fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + ord "a" - ord "A") else s;
-fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + ord "A" - ord "a") else s;
+fun to_ascii_lower s = if is_ascii_upper s then chr (ord s + Char.ord #"a" - Char.ord #"A") else s;
+fun to_ascii_upper s = if is_ascii_lower s then chr (ord s + Char.ord #"A" - Char.ord #"a") else s;
 
 fun is_ascii_identifier s =
   size s > 0 andalso is_ascii_letter (String.substring (s, 0, 1)) andalso
@@ -444,7 +444,7 @@
     fun bump [] = ["a"]
       | bump ("z" :: ss) = "a" :: bump ss
       | bump (s :: ss) =
-          if is_char s andalso ord "a" <= ord s andalso ord s < ord "z"
+          if is_char s andalso Char.ord #"a" <= ord s andalso ord s < Char.ord #"z"
           then chr (ord s + 1) :: ss
           else "a" :: s :: ss;
 
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -235,7 +235,8 @@
 
 val scan_escape =
   Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
-  $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
+  $$$ "^" @@@
+    (Scan.one (fn (s, _) => Char.ord #"@" <= ord s andalso ord s <= Char.ord #"_") >> single) ||
   Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
     Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
     Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/PIDE/yxml.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -49,12 +49,15 @@
 
 (* markers *)
 
-val X = chr 5;
-val Y = chr 6;
+val X_char = Char.chr 5;
+val Y_char = Char.chr 6;
+
+val X = String.str X_char;
+val Y = String.str Y_char;
 val XY = X ^ Y;
 val XYX = XY ^ X;
 
-val detect = exists_string (fn s => s = X orelse s = Y);
+fun detect s = Char.contains s X_char orelse Char.contains s Y_char;
 
 
 (* output *)
@@ -94,12 +97,10 @@
 
 (* splitting *)
 
-fun is_char s c = ord s = Char.ord c;
-
 val split_string =
   Substring.full #>
-  Substring.tokens (is_char X) #>
-  map (Substring.fields (is_char Y) #> map Substring.string);
+  Substring.tokens (fn c => c = X_char) #>
+  map (Substring.fields (fn c => c = Y_char) #> map Substring.string);
 
 
 (* structural errors *)
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -295,7 +295,7 @@
 val scan_vname =
   let
     fun nat n [] = n
-      | nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs;
+      | nat n (c :: cs) = nat (n * 10 + (ord c - Char.ord #"0")) cs;
 
     fun idxname cs ds = (implode (rev cs), nat 0 ds);
     fun chop_idx [] ds = idxname [] ds
@@ -371,9 +371,9 @@
 
 local
 
-val ten = ord "0" + 10;
-val a = ord "a";
-val A = ord "A";
+val ten = Char.ord #"0" + 10;
+val a = Char.ord #"a";
+val A = Char.ord #"A";
 val _ = a > A orelse raise Fail "Bad ASCII";
 
 fun remap_hex c =
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala	Mon Oct 17 19:03:13 2016 +0200
@@ -92,9 +92,16 @@
     val isabelle_tmp = Isabelle_System.tmp_dir("process")
     val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp))
 
+    val ml_runtime_options =
+    {
+      val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
+      if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
+      else ml_options ::: List("--gcthreads", options.int("threads").toString)
+    }
+
     // bash
     val bash_args =
-      Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
+      ml_runtime_options :::
       (eval_init ::: eval_modes ::: eval_options ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
diff -r 2e94501cbc34 -r a65ff5a84296 src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Oct 17 18:53:45 2016 +0200
+++ b/src/Pure/library.ML	Mon Oct 17 19:03:13 2016 +0200
@@ -596,7 +596,7 @@
 
 
 local
-  val zero = ord "0";
+  val zero = Char.ord #"0";
   val small_int = 10000: int;
   val small_int_table = Vector.tabulate (small_int, Int.toString);
 in
@@ -620,7 +620,7 @@
 
 fun read_radix_int radix cs =
   let
-    val zero = ord "0";
+    val zero = Char.ord #"0";
     val limit = zero + radix;
     fun scan (num, []) = (num, [])
       | scan (num, c :: cs) =