--- 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.
--- 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 =>
--- 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;
--- 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))
--- 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);
--- 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)
--- 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)
--- 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;
--- 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]);
--- 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 *)
--- 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 =
--- 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
--- 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) =