# HG changeset patch
# User wenzelm
# Date 1256656572 -3600
# Node ID 66eddea44a67d33c64df04b994335c471edf434e
# Parent  b207d84b64ad26cec5c8ada6283fe5aca75ff7b1# Parent  9a2911232c1b4753557262e6c49aba4f4053cc0b
merged

diff -r b207d84b64ad -r 66eddea44a67 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -297,7 +297,7 @@
 
           val tt' = tt |> fold upd all_names;
           val activate_simproc =
-              Output.no_warnings_CRITICAL
+              Output.no_warnings_CRITICAL   (* FIXME !?! *)
                (Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc]));
           val ctxt' =
               ctxt
diff -r b207d84b64ad -r 66eddea44a67 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/HOL/Tools/meson.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -323,7 +323,7 @@
   Strips universal quantifiers and breaks up conjunctions.
   Eliminates existential quantifiers using skoths: Skolemization theorems.*)
 fun cnf skoths ctxt (th,ths) =
-  let val ctxtr = Unsynchronized.ref ctxt
+  let val ctxtr = Unsynchronized.ref ctxt   (* FIXME ??? *)
       fun cnf_aux (th,ths) =
         if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
         else if not (has_conns ["All","Ex","op &"] (prop_of th))
diff -r b207d84b64ad -r 66eddea44a67 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -71,7 +71,7 @@
   prefix for the Skolem constant.*)
 fun declare_skofuns s th =
   let
-    val nref = Unsynchronized.ref 0
+    val nref = Unsynchronized.ref 0    (* FIXME ??? *)
     fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
           (*Existential: declare a Skolem function, then insert into body and continue*)
           let
@@ -87,7 +87,8 @@
             val (c, thy') =
               Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
             val cdef = cname ^ "_def"
-            val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
+            val thy'' =
+              Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
             val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
           in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
       | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx =
@@ -102,7 +103,7 @@
 
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun assume_skofuns s th =
-  let val sko_count = Unsynchronized.ref 0
+  let val sko_count = Unsynchronized.ref 0   (* FIXME ??? *)
       fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
             (*Existential: declare a Skolem function, then insert into body and continue*)
             let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
diff -r b207d84b64ad -r 66eddea44a67 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -90,6 +90,7 @@
 
     fun make_cpo admissible (type_def, below_def, set_def) theory =
       let
+        (* FIXME fold_rule might fold user input inintentionally *)
         val admissible' = fold_rule (the_list set_def) admissible;
         val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
         val theory' = theory
@@ -112,6 +113,7 @@
 
     fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
       let
+        (* FIXME fold_rule might fold user input inintentionally *)
         val UU_mem' = fold_rule (the_list set_def) UU_mem;
         val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
         val theory' = theory
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/General/file.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -90,10 +90,10 @@
     Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
 in
 
-fun check_cache (path, time) = CRITICAL (fn () =>
+fun check_cache (path, time) =
   (case Symtab.lookup (! ident_cache) path of
     NONE => NONE
-  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
+  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
 
 fun update_cache (path, (time, id)) = CRITICAL (fn () =>
   Unsynchronized.change ident_cache
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/General/print_mode.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -35,7 +35,7 @@
   let val modes =
     (case Thread.getLocal tag of
       SOME (SOME modes) => modes
-    | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
+    | _ => ! print_mode)
   in subtract (op =) [input, internal] modes end;
 
 fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -333,14 +333,14 @@
   Toplevel.keep (ProofContext.print_abbrevs o Toplevel.context_of);
 
 val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose
+  ProofContext.setmp_verbose_CRITICAL
     ProofContext.print_lthms (Toplevel.context_of state));
 
 val print_configs = Toplevel.unknown_context o Toplevel.keep (fn state =>
   Attrib.print_configs (Toplevel.context_of state));
 
 val print_theorems_proof = Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose
+  ProofContext.setmp_verbose_CRITICAL
     ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
 
 val print_theorems_theory = Toplevel.keep (fn state =>
@@ -431,10 +431,10 @@
 (* print proof context contents *)
 
 val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state));
+  ProofContext.setmp_verbose_CRITICAL ProofContext.print_binds (Toplevel.context_of state));
 
 val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose ProofContext.print_cases (Toplevel.context_of state));
+  ProofContext.setmp_verbose_CRITICAL ProofContext.print_cases (Toplevel.context_of state));
 
 
 (* print theorems, terms, types etc. *)
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -119,13 +119,13 @@
 in
 
 fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
-fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
+fun get_states () = ! global_states;
 
 fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
-fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
+fun get_commands () = ! global_commands;
 
 fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
-fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
+fun get_documents () = ! global_documents;
 
 fun init () = NAMED_CRITICAL "Isar" (fn () =>
  (global_states := Symtab.empty;
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -121,8 +121,8 @@
 
 in
 
-fun get_commands () = CRITICAL (fn () => ! global_commands);
-fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
+fun get_commands () = ! global_commands;
+fun get_lexicons () = ! global_lexicons;
 
 fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
 fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -101,8 +101,8 @@
 
 (* access current syntax *)
 
-fun get_commands () = CRITICAL (fn () => ! global_commands);
-fun get_markups () = CRITICAL (fn () => ! global_markups);
+fun get_commands () = ! global_commands;
+fun get_markups () = ! global_markups;
 
 fun get_command () = Symtab.lookup (get_commands ());
 fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -122,7 +122,7 @@
   val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
   val verbose: bool Unsynchronized.ref
-  val setmp_verbose: ('a -> 'b) -> 'a -> 'b
+  val setmp_verbose_CRITICAL: ('a -> 'b) -> 'a -> 'b
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
   val print_binds: Proof.context -> unit
@@ -1200,7 +1200,7 @@
 val verbose = Unsynchronized.ref false;
 fun verb f x = if ! verbose then f (x ()) else [];
 
-fun setmp_verbose f x = setmp_CRITICAL verbose true f x;
+fun setmp_verbose_CRITICAL f x = setmp_CRITICAL verbose true f x;
 
 
 (* local syntax *)
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -552,7 +552,7 @@
 local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
 
 fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
-fun get_hooks () = CRITICAL (fn () => ! hooks);
+fun get_hooks () = ! hooks;
 
 end;
 
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -54,7 +54,7 @@
 
 (* theorem bindings *)
 
-val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref [];
+val stored_thms: thm list Unsynchronized.ref = Unsynchronized.ref [];  (* FIXME via context!? *)
 
 fun ml_store sel (name, ths) =
   let
@@ -195,6 +195,7 @@
 fun eval_in ctxt verbose pos txt =
   Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) ();
 
+(* FIXME not thread-safe -- reference can be accessed directly *)
 fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
   let
     val _ = r := NONE;
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/System/isabelle_process.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -61,9 +61,6 @@
         else message_pos ts
     | _ => NONE);
 
-fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
-  (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
-
 in
 
 fun message _ _ "" = ()
@@ -74,14 +71,16 @@
           Position.properties_of (Position.thread_data ())
           |> Position.default_properties pos;
         val txt = clean_string [Symbol.STX] body;
-      in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
+        val msg = special ch ^ message_props props ^ txt ^ special_end ^ "\n";
+      in TextIO.output (out_stream, msg) end;
 
 fun init_message out_stream =
   let
     val pid = (Markup.pidN, process_id ());
     val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
     val text = Session.welcome ();
-  in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
+    val msg = special "A" ^ message_props [pid, session] ^ text ^ special_end ^ "\n";
+  in TextIO.output (out_stream, msg) end;
 
 end;
 
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/System/isar.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -47,10 +47,10 @@
       | edit n (st, hist) = edit (n - 1) (f st hist);
   in edit count (! global_state, ! global_history) end);
 
-fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
+fun state () = ! global_state;
 
-fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
-fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
+fun exn () = ! global_exn;
+fun set_exn exn =  global_exn := exn;
 
 end;
 
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/Thy/html.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -267,7 +267,7 @@
 (* document *)
 
 val charset = Unsynchronized.ref "ISO-8859-1";
-fun with_charset s = setmp_noncritical charset s;   (* FIXME *)
+fun with_charset s = setmp_noncritical charset s;   (* FIXME unreliable *)
 
 fun begin_document title =
   let val cs = ! charset in
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -41,16 +41,22 @@
 
 fun show_path () = map Path.implode (! load_path);
 
-fun del_path s = CRITICAL (fn () =>
-    Unsynchronized.change load_path (remove (op =) (Path.explode s)));
-fun add_path s = CRITICAL (fn () =>
-    (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
-fun path_add s = CRITICAL (fn () =>
+fun del_path s =
+  CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
+
+fun add_path s =
+  CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
+
+fun path_add s =
+  CRITICAL (fn () =>
     (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
+
 fun reset_path () = load_path := [Path.current];
 
 fun with_paths ss f x =
-  CRITICAL (fn () => setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
+  CRITICAL (fn () =>
+    setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
+
 fun with_path s f x = with_paths [s] f x;
 
 fun search_path dir path =
diff -r b207d84b64ad -r 66eddea44a67 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Oct 27 16:05:22 2009 +0100
+++ b/src/Pure/codegen.ML	Tue Oct 27 16:16:12 2009 +0100
@@ -105,7 +105,7 @@
 val quiet_mode = Unsynchronized.ref true;
 fun message s = if !quiet_mode then () else writeln s;
 
-val mode = Unsynchronized.ref ([] : string list);
+val mode = Unsynchronized.ref ([] : string list);   (* FIXME proper functional argument *)
 
 val margin = Unsynchronized.ref 80;
 
@@ -928,7 +928,7 @@
                 [str "(result ())"],
               str ");"]) ^
           "\n\nend;\n";
-        val _ = NAMED_CRITICAL "codegen" (fn () =>
+        val _ = NAMED_CRITICAL "codegen" (fn () =>   (* FIXME ??? *)
           ML_Context.eval_in (SOME ctxt) false Position.none s);
       in !eval_result end;
   in e () end;