--- a/src/Pure/Isar/runtime.ML Sat Mar 05 13:25:41 2016 +0100
+++ b/src/Pure/Isar/runtime.ML Sat Mar 05 13:51:21 2016 +0100
@@ -9,6 +9,7 @@
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)
@@ -37,6 +38,14 @@
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;
@@ -85,7 +94,7 @@
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
@@ -123,7 +132,7 @@
| 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));
@@ -150,7 +159,7 @@
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
--- a/src/Pure/ML/exn_debugger.ML Sat Mar 05 13:25:41 2016 +0100
+++ b/src/Pure/ML/exn_debugger.ML Sat Mar 05 13:51:21 2016 +0100
@@ -40,7 +40,7 @@
local
fun eq_exn exns =
- op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Output.position exns);
+ op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Properties.position exns);
in
fun capture_exception_trace e =
--- a/src/Pure/ML/exn_output.ML Sat Mar 05 13:25:41 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Title: Pure/ML/exn_output.ML
- Author: Makarius
-
-Auxiliary operations for exception output.
-*)
-
-signature EXN_OUTPUT =
-sig
- val position: exn -> Position.T
- val pretty: exn -> Pretty.T
-end;
-
-structure Exn_Output: EXN_OUTPUT =
-struct
-
-fun position exn =
- (case PolyML.exceptionLocation exn of
- NONE => Position.none
- | SOME loc => Exn_Properties.position_of loc);
-
-fun pretty (exn: exn) =
- Pretty.from_ML
- (ML_Pretty.from_polyml
- (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
-
-end;
--- a/src/Pure/ML/exn_properties.ML Sat Mar 05 13:25:41 2016 +0100
+++ b/src/Pure/ML/exn_properties.ML Sat Mar 05 13:51:21 2016 +0100
@@ -6,7 +6,8 @@
signature EXN_PROPERTIES =
sig
- val position_of: PolyML.location -> Position.T
+ val position_of_location: PolyML.location -> Position.T
+ val position: exn -> Position.T
val get: exn -> Properties.T
val update: Properties.entry list -> exn -> exn
end;
@@ -16,7 +17,7 @@
(* source locations *)
-fun props_of (loc: PolyML.location) =
+fun props_of_location (loc: PolyML.location) =
(case YXML.parse_body (#file loc) of
[] => []
| [XML.Text file] =>
@@ -24,12 +25,17 @@
else [(Markup.fileN, ML_System.standard_path file)]
| body => XML.Decode.properties body);
-fun position_of loc =
+fun position_of_location loc =
Position.make
{line = FixedInt.toInt (#startLine loc),
offset = FixedInt.toInt (#startPosition loc),
end_offset = FixedInt.toInt (#endPosition loc),
- props = props_of loc};
+ props = props_of_location loc};
+
+fun position exn =
+ (case PolyML.exceptionLocation exn of
+ NONE => Position.none
+ | SOME loc => position_of_location loc);
(* exception properties *)
@@ -37,14 +43,14 @@
fun get exn =
(case PolyML.exceptionLocation exn of
NONE => []
- | SOME loc => props_of loc);
+ | SOME loc => props_of_location loc);
fun update entries exn =
let
val loc =
the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
(PolyML.exceptionLocation exn);
- val props = props_of loc;
+ val props = props_of_location loc;
val props' = fold Properties.put entries props;
in
if props = props' then exn
--- a/src/Pure/ML/ml_compiler.ML Sat Mar 05 13:25:41 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Sat Mar 05 13:51:21 2016 +0100
@@ -38,7 +38,7 @@
(* parse trees *)
fun breakpoint_position loc =
- let val pos = Position.reset_range (Exn_Properties.position_of loc) in
+ let val pos = Position.reset_range (Exn_Properties.position_of_location loc) in
(case Position.offset_of pos of
NONE => pos
| SOME 1 => pos
@@ -60,7 +60,7 @@
(* syntax reports *)
fun reported_types loc types =
- let val pos = Exn_Properties.position_of loc in
+ let val pos = Exn_Properties.position_of_location loc in
is_reported pos ?
let
val xml =
@@ -72,8 +72,8 @@
fun reported_entity kind loc decl =
let
- val pos = Exn_Properties.position_of loc;
- val def_pos = Exn_Properties.position_of decl;
+ val pos = Exn_Properties.position_of_location loc;
+ val def_pos = Exn_Properties.position_of_location decl;
in
(is_reported pos andalso pos <> def_pos) ?
let
@@ -83,7 +83,7 @@
end;
fun reported_completions loc names =
- let val pos = Exn_Properties.position_of loc in
+ let val pos = Exn_Properties.position_of_location loc in
if is_reported pos andalso not (null names) then
let
val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
@@ -190,7 +190,7 @@
fun message {message = msg, hard, location = loc, context = _} =
let
- val pos = Exn_Properties.position_of loc;
+ val pos = Exn_Properties.position_of_location loc;
val txt =
(if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml msg));
@@ -275,7 +275,7 @@
(case exn of
STATIC_ERRORS () => ""
| Runtime.TOPLEVEL_ERROR => ""
- | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
+ | _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised");
val _ = output_warnings ();
val _ = output_writeln ();
in raise_error exn_msg end;
--- a/src/Pure/ROOT Sat Mar 05 13:25:41 2016 +0100
+++ b/src/Pure/ROOT Sat Mar 05 13:51:21 2016 +0100
@@ -101,7 +101,6 @@
"Isar/toplevel.ML"
"Isar/typedecl.ML"
"ML/exn_debugger.ML"
- "ML/exn_output.ML"
"ML/exn_properties.ML"
"ML/fixed_int_dummy.ML"
"ML/install_pp_polyml.ML"
--- a/src/Pure/ROOT.ML Sat Mar 05 13:25:41 2016 +0100
+++ b/src/Pure/ROOT.ML Sat Mar 05 13:51:21 2016 +0100
@@ -276,7 +276,6 @@
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
use "ML/ml_options.ML";
-use "ML/exn_output.ML";
use_no_debug "ML/exn_debugger.ML";
use "ML/ml_options.ML";
use_no_debug "Isar/runtime.ML";
--- a/src/Pure/Tools/debugger.ML Sat Mar 05 13:25:41 2016 +0100
+++ b/src/Pure/Tools/debugger.ML Sat Mar 05 13:51:21 2016 +0100
@@ -210,7 +210,7 @@
Output.protocol_message (Markup.debugger_state thread_name)
[get_debugging ()
|> map (fn st =>
- (Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
+ (Position.properties_of (Exn_Properties.position_of_location (ML_Debugger.debug_location st)),
ML_Debugger.debug_function st))
|> let open XML.Encode in list (pair properties string) end
|> YXML.string_of_body];