prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
authorwenzelm
Mon Apr 08 17:10:49 2013 +0200 (2013-04-08)
changeset 51639b7f908c99546
parent 51638 1275716f395b
child 51640 d022e8bd2375
prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);
src/Pure/Isar/runtime.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml.ML
     1.1 --- a/src/Pure/Isar/runtime.ML	Mon Apr 08 16:06:54 2013 +0200
     1.2 +++ b/src/Pure/Isar/runtime.ML	Mon Apr 08 17:10:49 2013 +0200
     1.3 @@ -12,10 +12,11 @@
     1.4    exception TOPLEVEL_ERROR
     1.5    val debug: bool Unsynchronized.ref
     1.6    val exn_context: Proof.context option -> exn -> exn
     1.7 +  type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T}
     1.8    type error = ((serial * string) * string option)
     1.9 -  val exn_messages_ids: (exn -> Position.T) -> exn -> error list
    1.10 -  val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
    1.11 -  val exn_message: (exn -> Position.T) -> exn -> string
    1.12 +  val exn_messages_ids: exn_info -> exn -> error list
    1.13 +  val exn_messages: exn_info -> exn -> (serial * string) list
    1.14 +  val exn_message: exn_info -> exn -> string
    1.15    val debugging: ('a -> 'b) -> 'a -> 'b
    1.16    val controlled_execution: ('a -> 'b) -> 'a -> 'b
    1.17    val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
    1.18 @@ -44,6 +45,7 @@
    1.19  
    1.20  (* exn_message *)
    1.21  
    1.22 +type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T};
    1.23  type error = ((serial * string) * string option);
    1.24  
    1.25  local
    1.26 @@ -67,7 +69,7 @@
    1.27  
    1.28  in
    1.29  
    1.30 -fun exn_messages_ids exn_position e =
    1.31 +fun exn_messages_ids {exn_position, pretty_exn} e =
    1.32    let
    1.33      fun raised exn name msgs =
    1.34        let val pos = Position.here (exn_position exn) in
    1.35 @@ -104,7 +106,7 @@
    1.36              | THM (msg, i, thms) =>
    1.37                  raised exn ("THM " ^ string_of_int i)
    1.38                    (msg :: if_context context Display.string_of_thm thms)
    1.39 -            | _ => raised exn (General.exnMessage exn) []);
    1.40 +            | _ => raised exn (Pretty.string_of (pretty_exn exn)) []);
    1.41          in [((i, msg), id)] end)
    1.42        and sorted_msgs context exn =
    1.43          sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
    1.44 @@ -113,11 +115,10 @@
    1.45  
    1.46  end;
    1.47  
    1.48 -fun exn_messages exn_position exn =
    1.49 -  map #1 (exn_messages_ids exn_position exn);
    1.50 +fun exn_messages exn_info exn = map #1 (exn_messages_ids exn_info exn);
    1.51  
    1.52 -fun exn_message exn_position exn =
    1.53 -  (case exn_messages exn_position exn of
    1.54 +fun exn_message exn_info exn =
    1.55 +  (case exn_messages exn_info exn of
    1.56      [] => "Interrupt"
    1.57    | msgs => cat_lines (map snd msgs));
    1.58  
     2.1 --- a/src/Pure/ML/ml_compiler.ML	Mon Apr 08 16:06:54 2013 +0200
     2.2 +++ b/src/Pure/ML/ml_compiler.ML	Mon Apr 08 17:10:49 2013 +0200
     2.3 @@ -6,7 +6,6 @@
     2.4  
     2.5  signature ML_COMPILER =
     2.6  sig
     2.7 -  val exn_position: exn -> Position.T
     2.8    val exn_messages_ids: exn -> Runtime.error list
     2.9    val exn_messages: exn -> (serial * string) list
    2.10    val exn_message: exn -> string
    2.11 @@ -16,10 +15,13 @@
    2.12  structure ML_Compiler: ML_COMPILER =
    2.13  struct
    2.14  
    2.15 -fun exn_position _ = Position.none;
    2.16 -val exn_messages_ids = Runtime.exn_messages_ids exn_position;
    2.17 -val exn_messages = Runtime.exn_messages exn_position;
    2.18 -val exn_message = Runtime.exn_message exn_position;
    2.19 +val exn_info =
    2.20 + {exn_position = fn _: exn => Position.none,
    2.21 +  pretty_exn = Pretty.str o General.exnMessage};
    2.22 +
    2.23 +val exn_messages_ids = Runtime.exn_messages_ids exn_info;
    2.24 +val exn_messages = Runtime.exn_messages exn_info;
    2.25 +val exn_message = Runtime.exn_message exn_info;
    2.26  
    2.27  fun eval verbose pos toks =
    2.28    let
     3.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Apr 08 16:06:54 2013 +0200
     3.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Apr 08 17:10:49 2013 +0200
     3.3 @@ -17,14 +17,25 @@
     3.4      Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
     3.5    end;
     3.6  
     3.7 +
     3.8 +(* exn_info *)
     3.9 +
    3.10  fun exn_position exn =
    3.11    (case PolyML.exceptionLocation exn of
    3.12      NONE => Position.none
    3.13    | SOME loc => position_of loc);
    3.14  
    3.15 -val exn_messages_ids = Runtime.exn_messages_ids exn_position;
    3.16 -val exn_messages = Runtime.exn_messages exn_position;
    3.17 -val exn_message = Runtime.exn_message exn_position;
    3.18 +fun pretty_exn (exn: exn) =
    3.19 +  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, get_print_depth ())));
    3.20 +
    3.21 +val exn_info = {exn_position = exn_position, pretty_exn = pretty_exn};
    3.22 +
    3.23 +
    3.24 +(* exn_message *)
    3.25 +
    3.26 +val exn_messages_ids = Runtime.exn_messages_ids exn_info;
    3.27 +val exn_messages = Runtime.exn_messages exn_info;
    3.28 +val exn_message = Runtime.exn_message exn_info;
    3.29  
    3.30  
    3.31  (* parse trees *)
    3.32 @@ -180,7 +191,7 @@
    3.33                (case exn of
    3.34                  STATIC_ERRORS () => ""
    3.35                | Runtime.TOPLEVEL_ERROR => ""
    3.36 -              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
    3.37 +              | _ => "Exception- " ^ Pretty.string_of (pretty_exn exn) ^ " raised");
    3.38              val _ = output_warnings ();
    3.39              val _ = output_writeln ();
    3.40            in raise_error exn_msg end;