# HG changeset patch
# User wenzelm
# Date 1137255258 -3600
# Node ID 725660906cb3cd1649dc1db67bdf97da341b545a
# Parent  38d72231b41d890759cc8812b25f55a8ff8c6460
sane ERROR vs. TOPLEVEL_ERROR handling;
added program;

diff -r 38d72231b41d -r 725660906cb3 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Jan 14 17:14:17 2006 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Jan 14 17:14:18 2006 +0100
@@ -94,6 +94,7 @@
   val command: transition -> state -> state
   val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a
   val excursion: transition list -> unit
+  val program: (unit -> 'a) -> 'a
   val set_state: state -> unit
   val get_state: unit -> state
   val exn: unit -> (exn * string) option
@@ -241,6 +242,12 @@
 exception EXCURSION_FAIL of exn * string;
 exception FAILURE of state * exn;
 
+fun debugging f x =
+  if ! debug then
+    setmp Library.do_transform_failure false
+      exception_trace (fn () => f x)
+  else f x;
+
 
 (* node transactions and recovery from stale theories *)
 
@@ -250,7 +257,7 @@
 
 fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
 
-val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
+val stale_theory = ERROR "Stale theory encountered after succesful execution!";
 
 fun checkpoint_node (Theory (thy, ctxt)) = Theory (Theory.checkpoint thy, ctxt)
   | checkpoint_node node = node;
@@ -261,12 +268,6 @@
 fun return (result, NONE) = result
   | return (result, SOME exn) = raise FAILURE (result, exn);
 
-fun debug_trans f x =
-  if ! debug then
-    setmp Output.transform_exceptions false
-      exception_trace (fn () => f x)
-  else f x;
-
 fun interruptible f x =
   let val y = ref x
   in raise_interrupt (fn () => y := f x) (); ! y end;
@@ -286,9 +287,9 @@
           cont_node
           |> (f
               |> (if hist then History.apply_copy copy_node else History.map)
-              |> debug_trans
+              |> debugging
               |> interruptible
-              |> transform_error)
+              |> setmp Output.do_toplevel_errors false)
           |> normal_state
           handle exn => error_state cont_node exn;
       in
@@ -345,7 +346,7 @@
 
 fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   | apply_union int (tr :: trs) state =
-      transform_error (apply_tr int tr) state
+      apply_tr int tr state
         handle UNDEF => apply_union int trs state
           | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
           | exn as FAILURE _ => raise exn
@@ -391,7 +392,7 @@
 fun at_command tr = command_msg "At " tr ^ ".";
 
 fun type_error tr state =
-  ERROR_MESSAGE (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
+  ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
 
 
 (* modify transitions *)
@@ -519,15 +520,12 @@
 fun exn_msg _ TERMINATE = "Exit."
   | exn_msg _ RESTART = "Restart."
   | exn_msg _ Interrupt = "Interrupt."
-  | exn_msg _ ERROR = "ERROR."
-  | exn_msg _ (ERROR_MESSAGE msg) = msg
+  | exn_msg _ Output.TOPLEVEL_ERROR = "Error."
+  | exn_msg _ (ERROR msg) = msg
   | exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   | exn_msg false (THEORY (msg, _)) = msg
   | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)
-  | exn_msg _ (ProofContext.CONTEXT (msg, _)) = msg
-  | exn_msg _ (Proof.STATE (msg, _)) = msg
-  | exn_msg _ (ProofHistory.FAIL msg) = msg
   | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
       fail_msg detailed "simproc" ((name, Position.none), exn)
   | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info
@@ -558,7 +556,7 @@
 fun exn_message exn = exn_msg (! debug) exn;
 
 fun print_exn NONE = ()
-  | print_exn (SOME (exn, s)) = error_msg (cat_lines [exn_message exn, s]);
+  | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
 
 end;
 
@@ -572,7 +570,7 @@
     val _ = conditional (not int andalso int_only) (fn () =>
       warning (command_msg "Interactive-only " tr));
 
-    fun do_timing f x = (info (command_msg "" tr); timeap f x);
+    fun do_timing f x = (Output.info (command_msg "" tr); timeap f x);
     fun do_profiling f x = profile (! profiling) f x;
 
     val (result, opt_exn) =
@@ -611,7 +609,7 @@
   | excur ((tr, pr) :: trs) (st, res) =
       (case apply (! interact) tr st of
         SOME (st', NONE) =>
-          excur trs (st', transform_error (fn () => pr st st' res) () handle exn =>
+          excur trs (st', pr st st' res handle exn =>
             raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr))
       | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info
       | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
@@ -623,7 +621,7 @@
 fun present_excursion trs res =
   (case excur trs (State NONE, res) of
     (State NONE, res') => res'
-  | _ => raise ERROR_MESSAGE "Unfinished development at end of input")
+  | _ => error "Unfinished development at end of input")
   handle exn => error (exn_message exn);
 
 fun excursion trs = present_excursion (map (rpair no_pr) trs) ();
@@ -631,6 +629,14 @@
 end;
 
 
+(* program: independent of state *)
+
+fun program f =
+  ((fn () => debugging f () handle exn => error (exn_message exn))
+    |> setmp Output.do_toplevel_errors true
+    |> Output.toplevel_errors) ();
+
+
 
 (** interactive transformations **)