src/Pure/Isar/runtime.ML
changeset 50914 fe4714886d92
parent 50911 ee7fe4230642
child 51242 a8e664e4fb5f
     1.1 --- a/src/Pure/Isar/runtime.ML	Wed Jan 16 20:40:50 2013 +0100
     1.2 +++ b/src/Pure/Isar/runtime.ML	Wed Jan 16 20:41:29 2013 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4    exception TOPLEVEL_ERROR
     1.5    val debug: bool Unsynchronized.ref
     1.6    val exn_context: Proof.context option -> exn -> exn
     1.7 +  val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list
     1.8    val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
     1.9    val exn_message: (exn -> Position.T) -> exn -> string
    1.10    val debugging: ('a -> 'b) -> 'a -> 'b
    1.11 @@ -42,22 +43,28 @@
    1.12  
    1.13  (* exn_message *)
    1.14  
    1.15 +local
    1.16 +
    1.17  fun if_context NONE _ _ = []
    1.18    | if_context (SOME ctxt) f xs = map (f ctxt) xs;
    1.19  
    1.20 -fun exn_messages exn_position e =
    1.21 +fun identify exn =
    1.22    let
    1.23 -    fun identify exn =
    1.24 -      let val exn' = Par_Exn.identify [] exn
    1.25 -      in (Par_Exn.the_serial exn', exn') end;
    1.26 +    val exn' = Par_Exn.identify [] exn;
    1.27 +    val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
    1.28 +  in ((Par_Exn.the_serial exn', exn'), exec_id) end;
    1.29  
    1.30 -    fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    1.31 -      | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    1.32 -      | flatten context exn =
    1.33 -          (case Par_Exn.dest exn of
    1.34 -            SOME exns => maps (flatten context) exns
    1.35 -          | NONE => [(context, identify exn)]);
    1.36 +fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
    1.37 +  | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
    1.38 +  | flatten context exn =
    1.39 +      (case Par_Exn.dest exn of
    1.40 +        SOME exns => maps (flatten context) exns
    1.41 +      | NONE => [(context, identify exn)]);
    1.42  
    1.43 +in
    1.44 +
    1.45 +fun exn_messages_ids exn_position e =
    1.46 +  let
    1.47      fun raised exn name msgs =
    1.48        let val pos = Position.here (exn_position exn) in
    1.49          (case msgs of
    1.50 @@ -66,10 +73,10 @@
    1.51          | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
    1.52        end;
    1.53  
    1.54 -    fun exn_msgs (context, (i, exn)) =
    1.55 +    fun exn_msgs (context, ((i, exn), id)) =
    1.56        (case exn of
    1.57          EXCURSION_FAIL (exn, loc) =>
    1.58 -          map (apsnd (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)))
    1.59 +          map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
    1.60              (sorted_msgs context exn)
    1.61        | _ =>
    1.62          let
    1.63 @@ -94,12 +101,17 @@
    1.64                  raised exn ("THM " ^ string_of_int i)
    1.65                    (msg :: if_context context Display.string_of_thm thms)
    1.66              | _ => raised exn (General.exnMessage exn) []);
    1.67 -        in [(i, msg)] end)
    1.68 +        in [((i, msg), id)] end)
    1.69        and sorted_msgs context exn =
    1.70 -        sort_distinct (int_ord o pairself fst) (maps exn_msgs (flatten context exn));
    1.71 +        sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
    1.72  
    1.73    in sorted_msgs NONE e end;
    1.74  
    1.75 +end;
    1.76 +
    1.77 +fun exn_messages exn_position exn =
    1.78 +  map #1 (exn_messages_ids exn_position exn);
    1.79 +
    1.80  fun exn_message exn_position exn =
    1.81    (case exn_messages exn_position exn of
    1.82      [] => "Interrupt"