# HG changeset patch
# User wenzelm
# Date 1185192372 -7200
# Node ID 707639e9497d96c15208935915a8249eefc5bae5
# Parent  947152add1538bcacf1bce14567bffb593ed04bf
marked some CRITICAL sections (for multithreading);

diff -r 947152add153 -r 707639e9497d src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/General/file.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -129,14 +129,14 @@
 
 in
 
-fun read path =
-  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path));
+fun read path = CRITICAL (fn () =>
+  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path)));
 
-fun write_list path txts =
-  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path));
+fun write_list path txts = CRITICAL (fn () =>
+  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path)));
 
-fun append_list path txts =
-  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path));
+fun append_list path txts = CRITICAL (fn () =>
+  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path)));
 
 fun write path txt = write_list path [txt];
 fun append path txt = append_list path [txt];
diff -r 947152add153 -r 707639e9497d src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/General/markup.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -163,8 +163,8 @@
   val default = {output = default_output};
   val modes = ref (Symtab.make [("", default)]);
 in
-  fun add_mode name output =
-    change modes (Symtab.update_new (name, {output = output}));
+  fun add_mode name output = CRITICAL (fn () =>
+    change modes (Symtab.update_new (name, {output = output})));
   fun get_mode () =
     the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
 end;
diff -r 947152add153 -r 707639e9497d src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -68,8 +68,8 @@
   val default = {output = default_output, escape = default_escape};
   val modes = ref (Symtab.make [("", default)]);
 in
-  fun add_mode name output escape =
-    change modes (Symtab.update_new (name, {output = output, escape = escape}));
+  fun add_mode name output escape = CRITICAL (fn () =>
+    change modes (Symtab.update_new (name, {output = output, escape = escape})));
   fun get_mode () =
     the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
 end;
@@ -86,8 +86,11 @@
 
 (* output primitives -- normally NOT used directly!*)
 
-fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
-fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
+fun std_output s = CRITICAL (fn () =>
+  (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
+
+fun std_error s = CRITICAL (fn () =>
+  (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
 
 val immediate_output = std_output o output;
 val writeln_default = std_output o suffix "\n";
diff -r 947152add153 -r 707639e9497d src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/General/pretty.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -90,8 +90,8 @@
   val default = {indent = default_indent};
   val modes = ref (Symtab.make [("", default)]);
 in
-  fun add_mode name indent =
-    change modes (Symtab.update_new (name, {indent = indent}));
+  fun add_mode name indent = CRITICAL (fn () =>
+    change modes (Symtab.update_new (name, {indent = indent})));
   fun get_mode () =
     the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
 end;
diff -r 947152add153 -r 707639e9497d src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/General/secure.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -39,12 +39,16 @@
 val orig_use_text = use_text;
 val orig_use_file = use_file;
 
-fun use_text name pr verbose txt = (secure_mltext (); orig_use_text name pr verbose txt);
-fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name);
-val use = use_file Output.ml_output true;
+fun use_text name pr verbose txt = CRITICAL (fn () =>
+  (secure_mltext (); orig_use_text name pr verbose txt));
+
+fun use_file pr verbose name = CRITICAL (fn () =>
+  (secure_mltext (); orig_use_file pr verbose name));
+
+fun use name = CRITICAL (fn () => use_file Output.ml_output true name);
 
 (*commit is dynamically bound!*)
-fun commit () = orig_use_text "" Output.ml_output false "commit();";
+fun commit () = CRITICAL (fn () => orig_use_text "" Output.ml_output false "commit();");
 
 
 (* shell commands *)
@@ -54,8 +58,8 @@
 val orig_execute = execute;
 val orig_system = system;
 
-fun execute s = (secure_shell (); orig_execute s);
-fun system s = (secure_shell (); orig_system s);
+fun execute s = CRITICAL (fn () => (secure_shell (); orig_execute s));
+fun system s = CRITICAL (fn () => (secure_shell (); orig_system s));
 
 end;
 
diff -r 947152add153 -r 707639e9497d src/Pure/General/susp.ML
--- a/src/Pure/General/susp.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/General/susp.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -28,17 +28,19 @@
 
 fun delay f = ref (Delay f);
 
-fun force (ref (Value v)) = v
-  | force (r as ref (Delay f)) =
+fun force susp = CRITICAL (fn () =>
+  (case ! susp of
+    Value v => v
+  | Delay f =>
       let
-        val v = f ()
-      in
-        r := Value v;
-        v
-      end;
+        val v = f ();
+        val _ = susp := Value v;
+      in v end));
 
-fun peek (ref (Value v)) = SOME v
-  | peek (ref (Delay _)) = NONE;
+fun peek susp =
+  (case ! susp of
+    Value v => SOME v
+  | Delay _ => NONE);
 
 fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
 
diff -r 947152add153 -r 707639e9497d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/Isar/method.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -343,11 +343,11 @@
 val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
 fun set_tactic f = tactic_ref := f;
 
-fun ml_tactic txt ctxt facts =
+fun ml_tactic txt ctxt = CRITICAL (fn () =>
   (ML_Context.use_mltext
     ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
       ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
-    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts);
+    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
 
 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
 fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
diff -r 947152add153 -r 707639e9497d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -455,9 +455,9 @@
 
 val prepare_dummies =
   let val next = ref 1 in
-    fn t =>
+    fn t => CRITICAL (fn () =>
       let val (i, u) = Term.replace_dummy_patterns (! next, t)
-      in next := i; u end
+      in next := i; u end)
   end;
 
 fun reject_dummies t = Term.no_dummy_patterns t
diff -r 947152add153 -r 707639e9497d src/Pure/compress.ML
--- a/src/Pure/compress.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/compress.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -36,7 +36,7 @@
 
 (* compress types *)
 
-fun typ thy =
+fun compress_typ thy =
   let
     val typs = #1 (CompressData.get thy);
     fun compress T =
@@ -47,10 +47,12 @@
           in change typs (Typtab.update (T', T')); T' end);
   in compress end;
 
+fun typ ty = CRITICAL (fn () => compress_typ ty);
+
 
 (* compress atomic terms *)
 
-fun term thy =
+fun compress_term thy =
   let
     val terms = #2 (CompressData.get thy);
     fun compress (t $ u) = compress t $ compress u
@@ -59,6 +61,8 @@
           (case Termtab.lookup (! terms) t of
             SOME t' => t'
           | NONE => (change terms (Termtab.update (t, t)); t));
-  in compress o map_types (typ thy) end;
+  in compress o map_types (compress_typ thy) end;
+
+fun term tm = CRITICAL (fn () => compress_term tm);
 
 end;
diff -r 947152add153 -r 707639e9497d src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/library.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -996,9 +996,9 @@
   val random_seed = ref 1.0;
 in
 
-fun random () =
-  let val r = rmod (a * !random_seed) m
-  in (random_seed := r; r) end;
+fun random () = CRITICAL (fn () =>
+  let val r = rmod (a * ! random_seed) m
+  in (random_seed := r; r) end);
 
 end;
 
@@ -1062,7 +1062,7 @@
 val gensym_seed = ref 0;
 
 in
-  fun gensym pre = pre ^ newid (inc gensym_seed);
+  fun gensym pre = pre ^ newid (CRITICAL (fn () => inc gensym_seed));
 end;
 
 
@@ -1073,7 +1073,7 @@
 
 type serial = int;
 local val count = ref 0
-in fun serial () = inc count end;
+in fun serial () = CRITICAL (fn () => inc count) end;
 
 val serial_string = string_of_int o serial;
 
diff -r 947152add153 -r 707639e9497d src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/tctical.ML	Mon Jul 23 14:06:12 2007 +0200
@@ -203,7 +203,7 @@
 (*Pause until a line is typed -- if non-empty then fail. *)
 fun pause_tac st =
   (tracing "** Press RETURN to continue:";
-   if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
+   if CRITICAL (fn () => TextIO.inputLine TextIO.stdIn) = SOME "\n" then Seq.single st
    else (tracing "Goodbye";  Seq.empty));
 
 exception TRACE_EXIT of thm
@@ -215,7 +215,7 @@
 
 (*Handle all tracing commands for current state and tactic *)
 fun exec_trace_command flag (tac, st) =
-   case TextIO.inputLine TextIO.stdIn of
+   case CRITICAL (fn () => TextIO.inputLine TextIO.stdIn) of
        SOME "\n" => tac st
      | SOME "f\n" => Seq.empty
      | SOME "o\n" => (flag:=false;  tac st)