--- a/src/Pure/General/output.ML Sun Apr 15 14:31:57 2007 +0200
+++ b/src/Pure/General/output.ML Sun Apr 15 14:31:59 2007 +0200
@@ -37,7 +37,6 @@
val tracing_fn: (string -> unit) ref
val warning_fn: (string -> unit) ref
val error_fn: (string -> unit) ref
- val panic_fn: (string -> unit) ref
val debug_fn: (string -> unit) ref
val debugging: bool ref
val no_warnings: ('a -> 'b) -> 'a -> 'b
@@ -45,7 +44,6 @@
val do_toplevel_errors: bool ref
val toplevel_errors: ('a -> 'b) -> 'a -> 'b
val ML_errors: ('a -> 'b) -> 'a -> 'b
- val panic: string -> unit
val debug: (unit -> string) -> unit
val error_msg: string -> unit
val ml_output: (string -> unit) * (string -> unit)
@@ -105,7 +103,6 @@
val tracing_fn = ref (fn s => ! writeln_fn s);
val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
-val panic_fn = ref (std_output o suffix "\n" o prefix_lines "!!! ");
val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
fun writeln s = ! writeln_fn (output s);
@@ -120,9 +117,6 @@
fun error_msg s = ! error_fn (output s);
-fun panic_msg s = ! panic_fn (output s);
-fun panic s = (panic_msg ("## SYSTEM EXIT ##\n" ^ s); exit 1);
-
val ml_output = (writeln, error_msg);
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Apr 15 14:31:57 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Apr 15 14:31:59 2007 +0200
@@ -108,9 +108,10 @@
Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
- Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
- Output.panic_fn := (fn s => decorate (special "364") (special "365") "!!! " s));
+ Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s));
+fun panic s =
+ (decorate (special "364") (special "365") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
fun emacs_notify s = decorate (special "360") (special "361") "" s;
@@ -274,8 +275,7 @@
val initialized = ref false;
-fun init false =
- Output.panic "No Proof General interface support for Isabelle/classic mode."
+fun init false = panic "No Proof General interface support for Isabelle/classic mode."
| init true =
(! initialized orelse
(Output.no_warnings init_outer_syntax ();
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Apr 15 14:31:57 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Apr 15 14:31:59 2007 +0200
@@ -214,9 +214,9 @@
Output.tracing_fn := (fn s => normalmsg Message Tracing false s);
Output.warning_fn := (fn s => errormsg Warning s);
Output.error_fn := (fn s => errormsg Fatal s);
- Output.panic_fn := (fn s => errormsg Panic s);
Output.debug_fn := (fn s => errormsg Debug s));
+fun panic s = (errormsg Panic ("## SYSTEM EXIT ##\n" ^ s); exit 1);
fun nonfatal_error s = errormsg Nonfatal s;
fun log_msg s = errormsg Log s;
@@ -399,8 +399,7 @@
val wwwpage =
(Url.explode (isabelle_www()))
handle ERROR _ =>
- (Output.panic
- ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
+ (panic ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
Url.explode isabellewww)
val proverinfo =
@@ -415,7 +414,7 @@
(issue_pgip proverinfo;
issue_pgip_rawtext (File.read path);
issue_pgip (lexicalstructure_keywords()))
- else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
+ else panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
end;
end
@@ -1064,7 +1063,7 @@
and handler (e,srco) =
case (e,srco) of
(XML_PARSE,SOME src) =>
- Output.panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
+ panic "Invalid XML input, aborting" (* TODO: attempt recovery *)
| (Interrupt,SOME src) =>
(Output.error_msg "Interrupt during PGIP processing"; loop true src)
| (Toplevel.UNDEF,SOME src) =>
@@ -1104,8 +1103,7 @@
val initialized = ref false;
-fun init_pgip false =
- Output.panic "No Proof General interface support for Isabelle/classic mode."
+fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
| init_pgip true =
(! initialized orelse
(Output.no_warnings init_outer_syntax ();