# 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;