src/Pure/Isar/runtime.ML

 signature RUNTIME =
 sig
   exception UNDEF
   exception EXCURSION_FAIL of exn * string
   exception TOPLEVEL_ERROR
+  val pretty_exn: exn -> Pretty.T
   val exn_context: Proof.context option -> exn -> exn
   val thread_context: exn -> exn
   type error = ((serial * string) * string option)
   val exn_messages_ids: exn -> error list
   val exn_messages: exn -> (serial * string) list

 exception UNDEF;
 exception EXCURSION_FAIL of exn * string;
 exception TOPLEVEL_ERROR;
 
 
+(* pretty *)
+
+fun pretty_exn (exn: exn) =
+  Pretty.from_ML
+    (ML_Pretty.from_polyml
+      (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
+
+
 (* exn_context *)
 
 exception CONTEXT of Proof.context * exn;
 
 fun exn_context NONE exn = exn

 in
 
 fun exn_messages_ids e =
   let
     fun raised exn name msgs =
-      let val pos = Position.here (Exn_Output.position exn) in
+      let val pos = Position.here (Exn_Properties.position exn) in
         (case msgs of
           [] => "exception " ^ name ^ " raised" ^ pos
         | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
         | _ =>
             cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") ::

                 raised exn "CTERM"
                   (msg :: robust_context context Syntax.string_of_term (map Thm.term_of cts))
             | THM (msg, i, thms) =>
                 raised exn ("THM " ^ string_of_int i)
                   (msg :: robust_context context Thm.string_of_thm thms)
-            | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
+            | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
         in [((i, msg), id)] end)
       and sorted_msgs context exn =
         sort_distinct (int_ord o apply2 (fst o fst)) (maps exn_msgs (flatten context exn));
 
   in sorted_msgs NONE e end;

 (* exception debugger *)
 
 local
 
 fun print_entry (name, loc) =
-  Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of loc));
+  Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_location loc));
 
 fun exception_debugger output e =
   let
     val (trace, result) = Exn_Debugger.capture_exception_trace e;
     val _ =