# HG changeset patch
# User wenzelm
# Date 1176640319 -7200
# Node ID 938c1011ac94cde9e7ead054183dec8cb332d62c
# Parent  7e6412e8d64bad7c874fa7963c10690b8548c8a6
removed unused Output.panic hook -- internal to PG wrapper;

diff -r 7e6412e8d64b -r 938c1011ac94 src/Pure/General/output.ML
--- 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);
 
 
diff -r 7e6412e8d64b -r 938c1011ac94 src/Pure/ProofGeneral/proof_general_emacs.ML
--- 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 ();
diff -r 7e6412e8d64b -r 938c1011ac94 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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 ();