# HG changeset patch
# User wenzelm
# Date 1117729798 -7200
# Node ID f58a4ff5d6dec53cf229ca34d64a3f4b7ee3f7bf
# Parent  abff174ba569e2b79c08ba3877431d71fb4a386c
tuned msgs;
exn_message: added Fail;
timing: info channel;

diff -r abff174ba569 -r f58a4ff5d6de src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jun 02 18:29:57 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Jun 02 18:29:58 2005 +0200
@@ -229,7 +229,7 @@
 
 fun check_stale state =
   if not (is_stale state) then ()
-  else warning "Stale signature encountered!  Should restart current theory.";
+  else warning "Stale signature encountered!";
 
 end;
 
@@ -466,6 +466,7 @@
   | exn_msg _ UnequalLengths = raised "UnequalLengths" []
   | exn_msg _ Empty = raised "Empty" []
   | exn_msg _ Subscript = raised "Subscript" []
+  | exn_msg _ (Fail msg) = raised "Fail" [msg]
   | exn_msg _ exn = General.exnMessage exn
 and fail_msg detailed kind ((name, pos), exn) =
   "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn;
@@ -494,7 +495,7 @@
       if int orelse not int_only then ()
       else warning (command_msg "Interactive-only " tr);
     val (result, opt_exn) =
-      (if ! Output.timing andalso not no_timing then (warning (command_msg "" tr); timeap) else I)
+      (if ! Output.timing andalso not no_timing then (info (command_msg "" tr); timeap) else I)
         (apply_trans int trans) state;
     val _ = if int andalso print andalso not (! quiet) then print_state false result else ();
   in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;