marked some CRITICAL sections (for multithreading);
authorwenzelm
Mon Jul 23 14:06:12 2007 +0200 (2007-07-23)
changeset 23922707639e9497d
parent 23921 947152add153
child 23923 8c10f3515633
marked some CRITICAL sections (for multithreading);
src/Pure/General/file.ML
src/Pure/General/markup.ML
src/Pure/General/output.ML
src/Pure/General/pretty.ML
src/Pure/General/secure.ML
src/Pure/General/susp.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
src/Pure/compress.ML
src/Pure/library.ML
src/Pure/tctical.ML
     1.1 --- a/src/Pure/General/file.ML	Mon Jul 23 14:06:11 2007 +0200
     1.2 +++ b/src/Pure/General/file.ML	Mon Jul 23 14:06:12 2007 +0200
     1.3 @@ -129,14 +129,14 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun read path =
     1.8 -  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path));
     1.9 +fun read path = CRITICAL (fn () =>
    1.10 +  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path)));
    1.11  
    1.12 -fun write_list path txts =
    1.13 -  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path));
    1.14 +fun write_list path txts = CRITICAL (fn () =>
    1.15 +  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path)));
    1.16  
    1.17 -fun append_list path txts =
    1.18 -  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path));
    1.19 +fun append_list path txts = CRITICAL (fn () =>
    1.20 +  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path)));
    1.21  
    1.22  fun write path txt = write_list path [txt];
    1.23  fun append path txt = append_list path [txt];
     2.1 --- a/src/Pure/General/markup.ML	Mon Jul 23 14:06:11 2007 +0200
     2.2 +++ b/src/Pure/General/markup.ML	Mon Jul 23 14:06:12 2007 +0200
     2.3 @@ -163,8 +163,8 @@
     2.4    val default = {output = default_output};
     2.5    val modes = ref (Symtab.make [("", default)]);
     2.6  in
     2.7 -  fun add_mode name output =
     2.8 -    change modes (Symtab.update_new (name, {output = output}));
     2.9 +  fun add_mode name output = CRITICAL (fn () =>
    2.10 +    change modes (Symtab.update_new (name, {output = output})));
    2.11    fun get_mode () =
    2.12      the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
    2.13  end;
     3.1 --- a/src/Pure/General/output.ML	Mon Jul 23 14:06:11 2007 +0200
     3.2 +++ b/src/Pure/General/output.ML	Mon Jul 23 14:06:12 2007 +0200
     3.3 @@ -68,8 +68,8 @@
     3.4    val default = {output = default_output, escape = default_escape};
     3.5    val modes = ref (Symtab.make [("", default)]);
     3.6  in
     3.7 -  fun add_mode name output escape =
     3.8 -    change modes (Symtab.update_new (name, {output = output, escape = escape}));
     3.9 +  fun add_mode name output escape = CRITICAL (fn () =>
    3.10 +    change modes (Symtab.update_new (name, {output = output, escape = escape})));
    3.11    fun get_mode () =
    3.12      the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
    3.13  end;
    3.14 @@ -86,8 +86,11 @@
    3.15  
    3.16  (* output primitives -- normally NOT used directly!*)
    3.17  
    3.18 -fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    3.19 -fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    3.20 +fun std_output s = CRITICAL (fn () =>
    3.21 +  (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
    3.22 +
    3.23 +fun std_error s = CRITICAL (fn () =>
    3.24 +  (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
    3.25  
    3.26  val immediate_output = std_output o output;
    3.27  val writeln_default = std_output o suffix "\n";
     4.1 --- a/src/Pure/General/pretty.ML	Mon Jul 23 14:06:11 2007 +0200
     4.2 +++ b/src/Pure/General/pretty.ML	Mon Jul 23 14:06:12 2007 +0200
     4.3 @@ -90,8 +90,8 @@
     4.4    val default = {indent = default_indent};
     4.5    val modes = ref (Symtab.make [("", default)]);
     4.6  in
     4.7 -  fun add_mode name indent =
     4.8 -    change modes (Symtab.update_new (name, {indent = indent}));
     4.9 +  fun add_mode name indent = CRITICAL (fn () =>
    4.10 +    change modes (Symtab.update_new (name, {indent = indent})));
    4.11    fun get_mode () =
    4.12      the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
    4.13  end;
     5.1 --- a/src/Pure/General/secure.ML	Mon Jul 23 14:06:11 2007 +0200
     5.2 +++ b/src/Pure/General/secure.ML	Mon Jul 23 14:06:12 2007 +0200
     5.3 @@ -39,12 +39,16 @@
     5.4  val orig_use_text = use_text;
     5.5  val orig_use_file = use_file;
     5.6  
     5.7 -fun use_text name pr verbose txt = (secure_mltext (); orig_use_text name pr verbose txt);
     5.8 -fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name);
     5.9 -val use = use_file Output.ml_output true;
    5.10 +fun use_text name pr verbose txt = CRITICAL (fn () =>
    5.11 +  (secure_mltext (); orig_use_text name pr verbose txt));
    5.12 +
    5.13 +fun use_file pr verbose name = CRITICAL (fn () =>
    5.14 +  (secure_mltext (); orig_use_file pr verbose name));
    5.15 +
    5.16 +fun use name = CRITICAL (fn () => use_file Output.ml_output true name);
    5.17  
    5.18  (*commit is dynamically bound!*)
    5.19 -fun commit () = orig_use_text "" Output.ml_output false "commit();";
    5.20 +fun commit () = CRITICAL (fn () => orig_use_text "" Output.ml_output false "commit();");
    5.21  
    5.22  
    5.23  (* shell commands *)
    5.24 @@ -54,8 +58,8 @@
    5.25  val orig_execute = execute;
    5.26  val orig_system = system;
    5.27  
    5.28 -fun execute s = (secure_shell (); orig_execute s);
    5.29 -fun system s = (secure_shell (); orig_system s);
    5.30 +fun execute s = CRITICAL (fn () => (secure_shell (); orig_execute s));
    5.31 +fun system s = CRITICAL (fn () => (secure_shell (); orig_system s));
    5.32  
    5.33  end;
    5.34  
     6.1 --- a/src/Pure/General/susp.ML	Mon Jul 23 14:06:11 2007 +0200
     6.2 +++ b/src/Pure/General/susp.ML	Mon Jul 23 14:06:12 2007 +0200
     6.3 @@ -28,17 +28,19 @@
     6.4  
     6.5  fun delay f = ref (Delay f);
     6.6  
     6.7 -fun force (ref (Value v)) = v
     6.8 -  | force (r as ref (Delay f)) =
     6.9 +fun force susp = CRITICAL (fn () =>
    6.10 +  (case ! susp of
    6.11 +    Value v => v
    6.12 +  | Delay f =>
    6.13        let
    6.14 -        val v = f ()
    6.15 -      in
    6.16 -        r := Value v;
    6.17 -        v
    6.18 -      end;
    6.19 +        val v = f ();
    6.20 +        val _ = susp := Value v;
    6.21 +      in v end));
    6.22  
    6.23 -fun peek (ref (Value v)) = SOME v
    6.24 -  | peek (ref (Delay _)) = NONE;
    6.25 +fun peek susp =
    6.26 +  (case ! susp of
    6.27 +    Value v => SOME v
    6.28 +  | Delay _ => NONE);
    6.29  
    6.30  fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
    6.31  
     7.1 --- a/src/Pure/Isar/method.ML	Mon Jul 23 14:06:11 2007 +0200
     7.2 +++ b/src/Pure/Isar/method.ML	Mon Jul 23 14:06:12 2007 +0200
     7.3 @@ -343,11 +343,11 @@
     7.4  val tactic_ref = ref ((fn _ => raise Match): Proof.context -> thm list -> tactic);
     7.5  fun set_tactic f = tactic_ref := f;
     7.6  
     7.7 -fun ml_tactic txt ctxt facts =
     7.8 +fun ml_tactic txt ctxt = CRITICAL (fn () =>
     7.9    (ML_Context.use_mltext
    7.10      ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
    7.11        ^ txt ^ "\nin Method.set_tactic tactic end") false (SOME (Context.Proof ctxt));
    7.12 -    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts);
    7.13 +    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
    7.14  
    7.15  fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
    7.16  fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
     8.1 --- a/src/Pure/Isar/proof_context.ML	Mon Jul 23 14:06:11 2007 +0200
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Jul 23 14:06:12 2007 +0200
     8.3 @@ -455,9 +455,9 @@
     8.4  
     8.5  val prepare_dummies =
     8.6    let val next = ref 1 in
     8.7 -    fn t =>
     8.8 +    fn t => CRITICAL (fn () =>
     8.9        let val (i, u) = Term.replace_dummy_patterns (! next, t)
    8.10 -      in next := i; u end
    8.11 +      in next := i; u end)
    8.12    end;
    8.13  
    8.14  fun reject_dummies t = Term.no_dummy_patterns t
     9.1 --- a/src/Pure/compress.ML	Mon Jul 23 14:06:11 2007 +0200
     9.2 +++ b/src/Pure/compress.ML	Mon Jul 23 14:06:12 2007 +0200
     9.3 @@ -36,7 +36,7 @@
     9.4  
     9.5  (* compress types *)
     9.6  
     9.7 -fun typ thy =
     9.8 +fun compress_typ thy =
     9.9    let
    9.10      val typs = #1 (CompressData.get thy);
    9.11      fun compress T =
    9.12 @@ -47,10 +47,12 @@
    9.13            in change typs (Typtab.update (T', T')); T' end);
    9.14    in compress end;
    9.15  
    9.16 +fun typ ty = CRITICAL (fn () => compress_typ ty);
    9.17 +
    9.18  
    9.19  (* compress atomic terms *)
    9.20  
    9.21 -fun term thy =
    9.22 +fun compress_term thy =
    9.23    let
    9.24      val terms = #2 (CompressData.get thy);
    9.25      fun compress (t $ u) = compress t $ compress u
    9.26 @@ -59,6 +61,8 @@
    9.27            (case Termtab.lookup (! terms) t of
    9.28              SOME t' => t'
    9.29            | NONE => (change terms (Termtab.update (t, t)); t));
    9.30 -  in compress o map_types (typ thy) end;
    9.31 +  in compress o map_types (compress_typ thy) end;
    9.32 +
    9.33 +fun term tm = CRITICAL (fn () => compress_term tm);
    9.34  
    9.35  end;
    10.1 --- a/src/Pure/library.ML	Mon Jul 23 14:06:11 2007 +0200
    10.2 +++ b/src/Pure/library.ML	Mon Jul 23 14:06:12 2007 +0200
    10.3 @@ -996,9 +996,9 @@
    10.4    val random_seed = ref 1.0;
    10.5  in
    10.6  
    10.7 -fun random () =
    10.8 -  let val r = rmod (a * !random_seed) m
    10.9 -  in (random_seed := r; r) end;
   10.10 +fun random () = CRITICAL (fn () =>
   10.11 +  let val r = rmod (a * ! random_seed) m
   10.12 +  in (random_seed := r; r) end);
   10.13  
   10.14  end;
   10.15  
   10.16 @@ -1062,7 +1062,7 @@
   10.17  val gensym_seed = ref 0;
   10.18  
   10.19  in
   10.20 -  fun gensym pre = pre ^ newid (inc gensym_seed);
   10.21 +  fun gensym pre = pre ^ newid (CRITICAL (fn () => inc gensym_seed));
   10.22  end;
   10.23  
   10.24  
   10.25 @@ -1073,7 +1073,7 @@
   10.26  
   10.27  type serial = int;
   10.28  local val count = ref 0
   10.29 -in fun serial () = inc count end;
   10.30 +in fun serial () = CRITICAL (fn () => inc count) end;
   10.31  
   10.32  val serial_string = string_of_int o serial;
   10.33  
    11.1 --- a/src/Pure/tctical.ML	Mon Jul 23 14:06:11 2007 +0200
    11.2 +++ b/src/Pure/tctical.ML	Mon Jul 23 14:06:12 2007 +0200
    11.3 @@ -203,7 +203,7 @@
    11.4  (*Pause until a line is typed -- if non-empty then fail. *)
    11.5  fun pause_tac st =
    11.6    (tracing "** Press RETURN to continue:";
    11.7 -   if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
    11.8 +   if CRITICAL (fn () => TextIO.inputLine TextIO.stdIn) = SOME "\n" then Seq.single st
    11.9     else (tracing "Goodbye";  Seq.empty));
   11.10  
   11.11  exception TRACE_EXIT of thm
   11.12 @@ -215,7 +215,7 @@
   11.13  
   11.14  (*Handle all tracing commands for current state and tactic *)
   11.15  fun exec_trace_command flag (tac, st) =
   11.16 -   case TextIO.inputLine TextIO.stdIn of
   11.17 +   case CRITICAL (fn () => TextIO.inputLine TextIO.stdIn) of
   11.18         SOME "\n" => tac st
   11.19       | SOME "f\n" => Seq.empty
   11.20       | SOME "o\n" => (flag:=false;  tac st)