1.1 --- a/src/Pure/General/file.ML	Sun Jul 29 16:00:06 2007 +0200
     1.2 +++ b/src/Pure/General/file.ML	Sun Jul 29 17:28:55 2007 +0200
     1.3 @@ -129,13 +129,13 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun read path = CRITICAL (fn () =>
     1.8 +fun read path = NAMED_CRITICAL "IO" (fn () =>
     1.9    fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path)));
    1.10  
    1.11 -fun write_list path txts = CRITICAL (fn () =>
    1.12 +fun write_list path txts = NAMED_CRITICAL "IO" (fn () =>
    1.13    fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path)));
    1.14  
    1.15 -fun append_list path txts = CRITICAL (fn () =>
    1.16 +fun append_list path txts = NAMED_CRITICAL "IO" (fn () =>
    1.17    fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path)));
    1.18  
    1.19  fun write path txt = write_list path [txt];

     2.1 --- a/src/Pure/General/output.ML	Sun Jul 29 16:00:06 2007 +0200
     2.2 +++ b/src/Pure/General/output.ML	Sun Jul 29 17:28:55 2007 +0200
     2.3 @@ -82,10 +82,10 @@
     2.4  
     2.5  (* output primitives -- normally NOT used directly!*)
     2.6  
     2.7 -fun std_output s = CRITICAL (fn () =>
     2.8 +fun std_output s = NAMED_CRITICAL "IO" (fn () =>
     2.9    (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
    2.10  
    2.11 -fun std_error s = CRITICAL (fn () =>
    2.12 +fun std_error s = NAMED_CRITICAL "IO" (fn () =>
    2.13    (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
    2.14  
    2.15  val immediate_output = std_output o output;

     3.1 --- a/src/Pure/General/print_mode.ML	Sun Jul 29 16:00:06 2007 +0200
     3.2 +++ b/src/Pure/General/print_mode.ML	Sun Jul 29 17:28:55 2007 +0200
     3.3 @@ -25,10 +25,11 @@
     3.4  val print_mode = ref ([]: string list);
     3.5  fun print_mode_active s = member (op =) (! print_mode) s;
     3.6  
     3.7 -fun with_modes modes f x = CRITICAL (fn () =>
     3.8 +fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
     3.9    setmp print_mode (modes @ ! print_mode) f x);
    3.10  
    3.11 -fun with_default f x = setmp print_mode [] f x;
    3.12 +fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
    3.13 +  setmp print_mode [] f x);
    3.14  
    3.15  end;
    3.16  

     4.1 --- a/src/Pure/General/secure.ML	Sun Jul 29 16:00:06 2007 +0200
     4.2 +++ b/src/Pure/General/secure.ML	Sun Jul 29 17:28:55 2007 +0200
     4.3 @@ -40,10 +40,10 @@
     4.4  val orig_use_text = use_text;
     4.5  val orig_use_file = use_file;
     4.6  
     4.7 -fun use_text name pr verbose txt = CRITICAL (fn () =>
     4.8 +fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () =>
     4.9    (secure_mltext (); orig_use_text name pr verbose txt));
    4.10  
    4.11 -fun use_file pr verbose name = CRITICAL (fn () =>
    4.12 +fun use_file pr verbose name = NAMED_CRITICAL "ML" (fn () =>
    4.13    (secure_mltext (); orig_use_file pr verbose name));
    4.14  
    4.15  fun use name = use_file Output.ml_output true name;
    4.16 @@ -62,8 +62,8 @@
    4.17  val orig_execute = execute;
    4.18  val orig_system = system;
    4.19  
    4.20 -fun execute s = CRITICAL (fn () => (secure_shell (); orig_execute s));
    4.21 -fun system s = CRITICAL (fn () => (secure_shell (); orig_system s));
    4.22 +fun execute s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_execute s));
    4.23 +fun system s = NAMED_CRITICAL "system" (fn () => (secure_shell (); orig_system s));
    4.24  
    4.25  end;
    4.26  

     5.1 --- a/src/Pure/General/source.ML	Sun Jul 29 16:00:06 2007 +0200
     5.2 +++ b/src/Pure/General/source.ML	Sun Jul 29 17:28:55 2007 +0200
     5.3 @@ -114,7 +114,7 @@
     5.4  
     5.5  (* stream source *)
     5.6  
     5.7 -fun slurp_input instream = CRITICAL (fn () =>
     5.8 +fun slurp_input instream = NAMED_CRITICAL "IO" (fn () =>
     5.9    let
    5.10      fun slurp () =
    5.11        (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of
    5.12 @@ -128,7 +128,7 @@
    5.13      if exists (fn c => c = "\n") input then (input, ())
    5.14      else
    5.15        (case
    5.16 -        CRITICAL (fn () =>
    5.17 +        NAMED_CRITICAL "IO" (fn () =>
    5.18            (TextIO.output (outstream, Output.output prompt);
    5.19              TextIO.flushOut outstream;
    5.20              TextIO.inputLine instream)) of

     6.1 --- a/src/Pure/General/susp.ML	Sun Jul 29 16:00:06 2007 +0200
     6.2 +++ b/src/Pure/General/susp.ML	Sun Jul 29 17:28:55 2007 +0200
     6.3 @@ -28,7 +28,7 @@
     6.4  
     6.5  fun delay f = ref (Delay f);
     6.6  
     6.7 -fun force susp = CRITICAL (fn () =>
     6.8 +fun force susp = NAMED_CRITICAL "susp" (fn () =>
     6.9    (case ! susp of
    6.10      Value v => v
    6.11    | Delay f =>

     7.1 --- a/src/Pure/Isar/toplevel.ML	Sun Jul 29 16:00:06 2007 +0200
     7.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Jul 29 17:28:55 2007 +0200
     7.3 @@ -719,7 +719,7 @@
     7.4  
     7.5  nonfix >> >>>;
     7.6  
     7.7 -fun >> tr = CRITICAL (fn () =>
     7.8 +fun >> tr = NAMED_CRITICAL "toplevel" (fn () =>
     7.9    (case apply true tr (get_state ()) of
    7.10      NONE => false
    7.11    | SOME (state', exn_info) =>

     8.1 --- a/src/Pure/compress.ML	Sun Jul 29 16:00:06 2007 +0200
     8.2 +++ b/src/Pure/compress.ML	Sun Jul 29 17:28:55 2007 +0200
     8.3 @@ -47,7 +47,7 @@
     8.4            in change typs (Typtab.update (T', T')); T' end);
     8.5    in compress end;
     8.6  
     8.7 -fun typ ty = CRITICAL (fn () => compress_typ ty);
     8.8 +fun typ ty = NAMED_CRITICAL "compress" (fn () => compress_typ ty);
     8.9  
    8.10  
    8.11  (* compress atomic terms *)
    8.12 @@ -63,6 +63,6 @@
    8.13            | NONE => (change terms (Termtab.update (t, t)); t));
    8.14    in compress o map_types (compress_typ thy) end;
    8.15  
    8.16 -fun term tm = CRITICAL (fn () => compress_term tm);
    8.17 +fun term tm = NAMED_CRITICAL "compress" (fn () => compress_term tm);
    8.18  
    8.19  end;