# HG changeset patch # User wenzelm # Date 1365433849 -7200 # Node ID b7f908c99546dd5a7a8a5531cd59bb330a16e57c # Parent 1275716f395b9bbf450861044c945de1c04e65a6 prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself); diff -r 1275716f395b -r b7f908c99546 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Mon Apr 08 16:06:54 2013 +0200 +++ b/src/Pure/Isar/runtime.ML Mon Apr 08 17:10:49 2013 +0200 @@ -12,10 +12,11 @@ exception TOPLEVEL_ERROR val debug: bool Unsynchronized.ref val exn_context: Proof.context option -> exn -> exn + type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T} type error = ((serial * string) * string option) - val exn_messages_ids: (exn -> Position.T) -> exn -> error list - val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list - val exn_message: (exn -> Position.T) -> exn -> string + val exn_messages_ids: exn_info -> exn -> error list + val exn_messages: exn_info -> exn -> (serial * string) list + val exn_message: exn_info -> exn -> string val debugging: ('a -> 'b) -> 'a -> 'b val controlled_execution: ('a -> 'b) -> 'a -> 'b val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b @@ -44,6 +45,7 @@ (* exn_message *) +type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T}; type error = ((serial * string) * string option); local @@ -67,7 +69,7 @@ in -fun exn_messages_ids exn_position e = +fun exn_messages_ids {exn_position, pretty_exn} e = let fun raised exn name msgs = let val pos = Position.here (exn_position exn) in @@ -104,7 +106,7 @@ | THM (msg, i, thms) => raised exn ("THM " ^ string_of_int i) (msg :: if_context context Display.string_of_thm thms) - | _ => raised exn (General.exnMessage exn) []); + | _ => raised exn (Pretty.string_of (pretty_exn exn)) []); in [((i, msg), id)] end) and sorted_msgs context exn = sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn)); @@ -113,11 +115,10 @@ end; -fun exn_messages exn_position exn = - map #1 (exn_messages_ids exn_position exn); +fun exn_messages exn_info exn = map #1 (exn_messages_ids exn_info exn); -fun exn_message exn_position exn = - (case exn_messages exn_position exn of +fun exn_message exn_info exn = + (case exn_messages exn_info exn of [] => "Interrupt" | msgs => cat_lines (map snd msgs)); diff -r 1275716f395b -r b7f908c99546 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Mon Apr 08 16:06:54 2013 +0200 +++ b/src/Pure/ML/ml_compiler.ML Mon Apr 08 17:10:49 2013 +0200 @@ -6,7 +6,6 @@ signature ML_COMPILER = sig - val exn_position: exn -> Position.T val exn_messages_ids: exn -> Runtime.error list val exn_messages: exn -> (serial * string) list val exn_message: exn -> string @@ -16,10 +15,13 @@ structure ML_Compiler: ML_COMPILER = struct -fun exn_position _ = Position.none; -val exn_messages_ids = Runtime.exn_messages_ids exn_position; -val exn_messages = Runtime.exn_messages exn_position; -val exn_message = Runtime.exn_message exn_position; +val exn_info = + {exn_position = fn _: exn => Position.none, + pretty_exn = Pretty.str o General.exnMessage}; + +val exn_messages_ids = Runtime.exn_messages_ids exn_info; +val exn_messages = Runtime.exn_messages exn_info; +val exn_message = Runtime.exn_message exn_info; fun eval verbose pos toks = let diff -r 1275716f395b -r b7f908c99546 src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Mon Apr 08 16:06:54 2013 +0200 +++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Apr 08 17:10:49 2013 +0200 @@ -17,14 +17,25 @@ Position.make {line = line, offset = offset, end_offset = end_offset, props = props} end; + +(* exn_info *) + fun exn_position exn = (case PolyML.exceptionLocation exn of NONE => Position.none | SOME loc => position_of loc); -val exn_messages_ids = Runtime.exn_messages_ids exn_position; -val exn_messages = Runtime.exn_messages exn_position; -val exn_message = Runtime.exn_message exn_position; +fun pretty_exn (exn: exn) = + Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, get_print_depth ()))); + +val exn_info = {exn_position = exn_position, pretty_exn = pretty_exn}; + + +(* exn_message *) + +val exn_messages_ids = Runtime.exn_messages_ids exn_info; +val exn_messages = Runtime.exn_messages exn_info; +val exn_message = Runtime.exn_message exn_info; (* parse trees *) @@ -180,7 +191,7 @@ (case exn of STATIC_ERRORS () => "" | Runtime.TOPLEVEL_ERROR => "" - | _ => "Exception- " ^ General.exnMessage exn ^ " raised"); + | _ => "Exception- " ^ Pretty.string_of (pretty_exn exn) ^ " raised"); val _ = output_warnings (); val _ = output_writeln (); in raise_error exn_msg end;