--- a/src/Pure/General/exn.ML Sat Apr 02 21:54:51 2016 +0200
+++ b/src/Pure/General/exn.ML Sat Apr 02 21:55:32 2016 +0200
@@ -14,6 +14,7 @@
signature EXN =
sig
include BASIC_EXN
+ val polyml_location: exn -> PolyML.location option
val reraise: exn -> 'a
datatype 'a result = Res of 'a | Exn of exn
val get_res: 'a result -> 'a option
@@ -38,12 +39,11 @@
structure Exn: EXN =
struct
-(* reraise *)
+(* location *)
-fun reraise exn =
- (case PolyML.exceptionLocation exn of
- NONE => raise exn
- | SOME location => PolyML.raiseWithLocation (exn, location));
+val polyml_location = PolyML.Exception.exceptionLocation;
+
+val reraise = PolyML.Exception.reraise;
(* user errors *)
--- a/src/Pure/Isar/runtime.ML Sat Apr 02 21:54:51 2016 +0200
+++ b/src/Pure/Isar/runtime.ML Sat Apr 02 21:55:32 2016 +0200
@@ -159,7 +159,7 @@
local
fun print_entry (name, loc) =
- Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_location loc));
+ Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_polyml_location loc));
fun exception_debugger output e =
let
--- a/src/Pure/ML/exn_debugger.ML Sat Apr 02 21:54:51 2016 +0200
+++ b/src/Pure/ML/exn_debugger.ML Sat Apr 02 21:55:32 2016 +0200
@@ -6,7 +6,8 @@
signature EXN_DEBUGGER =
sig
- val capture_exception_trace: (unit -> 'a) -> (string * ML_Debugger.location) list * 'a Exn.result
+ val capture_exception_trace:
+ (unit -> 'a) -> (string * ML_Compiler0.polyml_location) list * 'a Exn.result
end;
structure Exn_Debugger: EXN_DEBUGGER =
@@ -15,7 +16,8 @@
(* thread data *)
local
- val tag = Universal.tag () : ((string * ML_Debugger.location) * exn) list option Universal.tag;
+ val tag =
+ Universal.tag () : ((string * ML_Compiler0.polyml_location) * exn) list option Universal.tag;
in
fun start_trace () = Thread.setLocal (tag, SOME []);
--- a/src/Pure/ML/exn_properties.ML Sat Apr 02 21:54:51 2016 +0200
+++ b/src/Pure/ML/exn_properties.ML Sat Apr 02 21:55:32 2016 +0200
@@ -6,7 +6,7 @@
signature EXN_PROPERTIES =
sig
- val position_of_location: PolyML.location -> Position.T
+ val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T
val position: exn -> Position.T
val get: exn -> Properties.T
val update: Properties.entry list -> exn -> exn
@@ -17,7 +17,7 @@
(* source locations *)
-fun props_of_location (loc: PolyML.location) =
+fun props_of_polyml_location (loc: ML_Compiler0.polyml_location) =
(case YXML.parse_body (#file loc) of
[] => []
| [XML.Text file] =>
@@ -25,25 +25,25 @@
else [(Markup.fileN, ML_System.standard_path file)]
| body => XML.Decode.properties body);
-fun position_of_location loc =
+fun position_of_polyml_location loc =
Position.make
{line = FixedInt.toInt (#startLine loc),
offset = FixedInt.toInt (#startPosition loc),
end_offset = FixedInt.toInt (#endPosition loc),
- props = props_of_location loc};
+ props = props_of_polyml_location loc};
fun position exn =
- (case PolyML.exceptionLocation exn of
+ (case Exn.polyml_location exn of
NONE => Position.none
- | SOME loc => position_of_location loc);
+ | SOME loc => position_of_polyml_location loc);
(* exception properties *)
fun get exn =
- (case PolyML.exceptionLocation exn of
+ (case Exn.polyml_location exn of
NONE => []
- | SOME loc => props_of_location loc);
+ | SOME loc => props_of_polyml_location loc);
fun update entries exn =
if Exn.is_interrupt exn then exn
@@ -51,8 +51,8 @@
let
val loc =
the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
- (PolyML.exceptionLocation exn);
- val props = props_of_location loc;
+ (Exn.polyml_location exn);
+ val props = props_of_polyml_location loc;
val props' = fold Properties.put entries props;
in
if props = props' then exn
--- a/src/Pure/ML/ml_compiler.ML Sat Apr 02 21:54:51 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML Sat Apr 02 21:55:32 2016 +0200
@@ -38,7 +38,7 @@
(* parse trees *)
fun breakpoint_position loc =
- let val pos = Position.no_range_position (Exn_Properties.position_of_location loc) in
+ let val pos = Position.no_range_position (Exn_Properties.position_of_polyml_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_location loc in
+ let val pos = Exn_Properties.position_of_polyml_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_location loc;
- val def_pos = Exn_Properties.position_of_location decl;
+ val pos = Exn_Properties.position_of_polyml_location loc;
+ val def_pos = Exn_Properties.position_of_polyml_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_location loc in
+ let val pos = Exn_Properties.position_of_polyml_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);
@@ -189,7 +189,7 @@
fun message {message = msg, hard, location = loc, context = _} =
let
- val pos = Exn_Properties.position_of_location loc;
+ val pos = Exn_Properties.position_of_polyml_location loc;
val txt =
(if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
Pretty.string_of (Pretty.from_polyml msg);
--- a/src/Pure/ML/ml_compiler0.ML Sat Apr 02 21:54:51 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML Sat Apr 02 21:55:32 2016 +0200
@@ -7,6 +7,7 @@
signature ML_COMPILER0 =
sig
+ type polyml_location = PolyML.location
type context =
{name_space: ML_Name_Space.T,
print_depth: int option,
@@ -24,6 +25,9 @@
structure ML_Compiler0: ML_COMPILER0 =
struct
+type polyml_location = PolyML.location;
+
+
(* global options *)
val _ = PolyML.Compiler.reportUnreferencedIds := true;
--- a/src/Pure/ML/ml_debugger.ML Sat Apr 02 21:54:51 2016 +0200
+++ b/src/Pure/ML/ml_debugger.ML Sat Apr 02 21:55:32 2016 +0200
@@ -10,17 +10,16 @@
val exn_id: exn -> exn_id
val print_exn_id: exn_id -> string
val eq_exn_id: exn_id * exn_id -> bool
- type location
- val on_entry: (string * location -> unit) option -> unit
- val on_exit: (string * location -> unit) option -> unit
- val on_exit_exception: (string * location -> exn -> unit) option -> unit
- val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
+ val on_entry: (string * ML_Compiler0.polyml_location -> unit) option -> unit
+ val on_exit: (string * ML_Compiler0.polyml_location -> unit) option -> unit
+ val on_exit_exception: (string * ML_Compiler0.polyml_location -> exn -> unit) option -> unit
+ val on_breakpoint: (ML_Compiler0.polyml_location * bool Unsynchronized.ref -> unit) option -> unit
type state
val state: Thread.thread -> state list
val debug_function: state -> string
val debug_function_arg: state -> ML_Name_Space.valueVal
val debug_function_result: state -> ML_Name_Space.valueVal
- val debug_location: state -> location
+ val debug_location: state -> ML_Compiler0.polyml_location
val debug_name_space: state -> ML_Name_Space.T
val debug_local_name_space: state -> ML_Name_Space.T
end;
@@ -49,8 +48,6 @@
(* hooks *)
-type location = PolyML.location;
-
val on_entry = PolyML.DebuggerInterface.setOnEntry;
val on_exit = PolyML.DebuggerInterface.setOnExit;
val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
--- a/src/Pure/Tools/debugger.ML Sat Apr 02 21:54:51 2016 +0200
+++ b/src/Pure/Tools/debugger.ML Sat Apr 02 21:55:32 2016 +0200
@@ -209,7 +209,8 @@
Output.protocol_message (Markup.debugger_state thread_name)
[get_debugging ()
|> map (fn st =>
- (Position.properties_of (Exn_Properties.position_of_location (ML_Debugger.debug_location st)),
+ (Position.properties_of
+ (Exn_Properties.position_of_polyml_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];