1.1 --- a/src/HOL/Mirabelle/Mirabelle.thy Mon Sep 06 12:38:45 2010 +0200
1.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy Mon Sep 06 13:06:27 2010 +0200
1.3 @@ -7,7 +7,7 @@
1.4 uses "Tools/mirabelle.ML"
1.5 begin
1.6
1.7 -(* no multithreading, no parallel proofs *)
1.8 +(* no multithreading, no parallel proofs *) (* FIXME *)
1.9 ML {* Multithreading.max_threads := 1 *}
1.10 ML {* Goal.parallel_proofs := 0 *}
1.11
2.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Sep 06 12:38:45 2010 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Sep 06 13:06:27 2010 +0200
2.3 @@ -348,7 +348,7 @@
2.4 |>> curry (op =) "genuine")
2.5 in
2.6 if auto orelse blocking then go ()
2.7 - else (Toplevel.thread true (tap go); (false, state))
2.8 + else (Toplevel.thread true (tap go); (false, state)) (* FIXME no threads in user-space *)
2.9 end
2.10
2.11 fun nitpick_trans (params, i) =
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Sep 06 12:38:45 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Sep 06 13:06:27 2010 +0200
3.3 @@ -452,6 +452,7 @@
3.4 else
3.5 ()
3.6 end
3.7 + (* FIXME no threads in user-space *)
3.8 in if blocking then run () else Toplevel.thread true (tap run) |> K () end
3.9
3.10 val setup =
4.1 --- a/src/HOL/ex/ROOT.ML Mon Sep 06 12:38:45 2010 +0200
4.2 +++ b/src/HOL/ex/ROOT.ML Mon Sep 06 13:06:27 2010 +0200
4.3 @@ -70,7 +70,7 @@
4.4 HTML.with_charset "utf-8" (no_document use_thys)
4.5 ["Hebrew", "Chinese", "Serbian"];
4.6
4.7 -(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
4.8 +(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy)) (* FIXME *)
4.9 "Hilbert_Classical";
4.10
4.11 use_thy "SVC_Oracle";
5.1 --- a/src/Tools/WWW_Find/scgi_server.ML Mon Sep 06 12:38:45 2010 +0200
5.2 +++ b/src/Tools/WWW_Find/scgi_server.ML Mon Sep 06 13:06:27 2010 +0200
5.3 @@ -50,7 +50,7 @@
5.4 else (tracing ("Waiting for a free thread...");
5.5 ConditionVar.wait (thread_wait, thread_wait_mutex));
5.6 add_thread
5.7 - (Thread.fork
5.8 + (Thread.fork (* FIXME avoid low-level Poly/ML thread primitives *)
5.9 (fn () => exception_trace threadf,
5.10 [Thread.EnableBroadcastInterrupt true,
5.11 Thread.InterruptState