# HG changeset patch
# User wenzelm
# Date 1185722935 -7200
# Node ID 81aafd4656621f9edb8d7bd567af96972fde7b7f
# Parent  f4266556180176c53ac96544d6f8ef192aa371fc
NAMED_CRITICAL;

diff -r f42665561801 -r 81aafd465662 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/General/file.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -129,13 +129,13 @@
 
 in
 
-fun read path = CRITICAL (fn () =>
+fun read path = NAMED_CRITICAL "IO" (fn () =>
   fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path)));
 
-fun write_list path txts = CRITICAL (fn () =>
+fun write_list path txts = NAMED_CRITICAL "IO" (fn () =>
   fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path)));
 
-fun append_list path txts = CRITICAL (fn () =>
+fun append_list path txts = NAMED_CRITICAL "IO" (fn () =>
   fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path)));
 
 fun write path txt = write_list path [txt];
diff -r f42665561801 -r 81aafd465662 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/General/output.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -82,10 +82,10 @@
 
 (* output primitives -- normally NOT used directly!*)
 
-fun std_output s = CRITICAL (fn () =>
+fun std_output s = NAMED_CRITICAL "IO" (fn () =>
   (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
 
-fun std_error s = CRITICAL (fn () =>
+fun std_error s = NAMED_CRITICAL "IO" (fn () =>
   (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
 
 val immediate_output = std_output o output;
diff -r f42665561801 -r 81aafd465662 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/General/print_mode.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -25,10 +25,11 @@
 val print_mode = ref ([]: string list);
 fun print_mode_active s = member (op =) (! print_mode) s;
 
-fun with_modes modes f x = CRITICAL (fn () =>
+fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
   setmp print_mode (modes @ ! print_mode) f x);
 
-fun with_default f x = setmp print_mode [] f x;
+fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
+  setmp print_mode [] f x);
 
 end;
 
diff -r f42665561801 -r 81aafd465662 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/General/secure.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -40,10 +40,10 @@
 val orig_use_text = use_text;
 val orig_use_file = use_file;
 
-fun use_text name pr verbose txt = CRITICAL (fn () =>
+fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () =>
   (secure_mltext (); orig_use_text name pr verbose txt));
 
-fun use_file pr verbose name = CRITICAL (fn () =>
+fun use_file pr verbose name = NAMED_CRITICAL "ML" (fn () =>
   (secure_mltext (); orig_use_file pr verbose name));
 
 fun use name = use_file Output.ml_output true name;
@@ -62,8 +62,8 @@
 val orig_execute = execute;
 val orig_system = system;
 
-fun execute s = CRITICAL (fn () => (secure_shell (); orig_execute s));
-fun system s = CRITICAL (fn () => (secure_shell (); orig_system s));
+fun execute s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_execute s));
+fun system s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_system s));
 
 end;
 
diff -r f42665561801 -r 81aafd465662 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/General/source.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -114,7 +114,7 @@
 
 (* stream source *)
 
-fun slurp_input instream = CRITICAL (fn () =>
+fun slurp_input instream = NAMED_CRITICAL "IO" (fn () =>
   let
     fun slurp () =
       (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of
@@ -128,7 +128,7 @@
     if exists (fn c => c = "\n") input then (input, ())
     else
       (case
-        CRITICAL (fn () =>
+        NAMED_CRITICAL "IO" (fn () =>
           (TextIO.output (outstream, Output.output prompt);
             TextIO.flushOut outstream;
             TextIO.inputLine instream)) of
diff -r f42665561801 -r 81aafd465662 src/Pure/General/susp.ML
--- a/src/Pure/General/susp.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/General/susp.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -28,7 +28,7 @@
 
 fun delay f = ref (Delay f);
 
-fun force susp = CRITICAL (fn () =>
+fun force susp = NAMED_CRITICAL "susp" (fn () =>
   (case ! susp of
     Value v => v
   | Delay f =>
diff -r f42665561801 -r 81aafd465662 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -719,7 +719,7 @@
 
 nonfix >> >>>;
 
-fun >> tr = CRITICAL (fn () =>
+fun >> tr = NAMED_CRITICAL "toplevel" (fn () =>
   (case apply true tr (get_state ()) of
     NONE => false
   | SOME (state', exn_info) =>
diff -r f42665561801 -r 81aafd465662 src/Pure/compress.ML
--- a/src/Pure/compress.ML	Sun Jul 29 16:00:06 2007 +0200
+++ b/src/Pure/compress.ML	Sun Jul 29 17:28:55 2007 +0200
@@ -47,7 +47,7 @@
           in change typs (Typtab.update (T', T')); T' end);
   in compress end;
 
-fun typ ty = CRITICAL (fn () => compress_typ ty);
+fun typ ty = NAMED_CRITICAL "compress" (fn () => compress_typ ty);
 
 
 (* compress atomic terms *)
@@ -63,6 +63,6 @@
           | NONE => (change terms (Termtab.update (t, t)); t));
   in compress o map_types (compress_typ thy) end;
 
-fun term tm = CRITICAL (fn () => compress_term tm);
+fun term tm = NAMED_CRITICAL "compress" (fn () => compress_term tm);
 
 end;