# HG changeset patch
# User wenzelm
# Date 1283771187 -7200
# Node ID 3e94ebe282f1075bae869c12fe6f810576ba3564
# Parent  14b16b380ca18c5535eb9cd811e2635d65a0b885
some results of concurrency code inspection;

diff -r 14b16b380ca1 -r 3e94ebe282f1 src/HOL/Mirabelle/Mirabelle.thy
--- a/src/HOL/Mirabelle/Mirabelle.thy	Mon Sep 06 12:38:45 2010 +0200
+++ b/src/HOL/Mirabelle/Mirabelle.thy	Mon Sep 06 13:06:27 2010 +0200
@@ -7,7 +7,7 @@
 uses "Tools/mirabelle.ML"
 begin
 
-(* no multithreading, no parallel proofs *)
+(* no multithreading, no parallel proofs *)  (* FIXME *)
 ML {* Multithreading.max_threads := 1 *}
 ML {* Goal.parallel_proofs := 0 *}
 
diff -r 14b16b380ca1 -r 3e94ebe282f1 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 06 12:38:45 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Sep 06 13:06:27 2010 +0200
@@ -348,7 +348,7 @@
                            |>> curry (op =) "genuine")
   in
     if auto orelse blocking then go ()
-    else (Toplevel.thread true (tap go); (false, state))
+    else (Toplevel.thread true (tap go); (false, state))  (* FIXME no threads in user-space *)
   end
 
 fun nitpick_trans (params, i) =
diff -r 14b16b380ca1 -r 3e94ebe282f1 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Sep 06 12:38:45 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Sep 06 13:06:27 2010 +0200
@@ -452,6 +452,7 @@
             else
               ()
           end
+      (* FIXME no threads in user-space *)
       in if blocking then run () else Toplevel.thread true (tap run) |> K () end
 
 val setup =
diff -r 14b16b380ca1 -r 3e94ebe282f1 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Mon Sep 06 12:38:45 2010 +0200
+++ b/src/HOL/ex/ROOT.ML	Mon Sep 06 13:06:27 2010 +0200
@@ -70,7 +70,7 @@
 HTML.with_charset "utf-8" (no_document use_thys)
   ["Hebrew", "Chinese", "Serbian"];
 
-(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
+(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))  (* FIXME *)
   "Hilbert_Classical";
 
 use_thy "SVC_Oracle";
diff -r 14b16b380ca1 -r 3e94ebe282f1 src/Tools/WWW_Find/scgi_server.ML
--- a/src/Tools/WWW_Find/scgi_server.ML	Mon Sep 06 12:38:45 2010 +0200
+++ b/src/Tools/WWW_Find/scgi_server.ML	Mon Sep 06 13:06:27 2010 +0200
@@ -50,7 +50,7 @@
        else (tracing ("Waiting for a free thread...");
              ConditionVar.wait (thread_wait, thread_wait_mutex));
        add_thread
-         (Thread.fork
+         (Thread.fork   (* FIXME avoid low-level Poly/ML thread primitives *)
             (fn () => exception_trace threadf,
              [Thread.EnableBroadcastInterrupt true,
               Thread.InterruptState