# HG changeset patch
# User wenzelm
# Date 1459626932 -7200
# Node ID 48c24d0b6d85012a29a15d328745a8091ac7b8d3
# Parent  5c678ee5d34a5e6624111c76b175960f6a277936
tuned signature;

diff -r 5c678ee5d34a -r 48c24d0b6d85 src/Pure/General/exn.ML
--- 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 *)
diff -r 5c678ee5d34a -r 48c24d0b6d85 src/Pure/Isar/runtime.ML
--- 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
diff -r 5c678ee5d34a -r 48c24d0b6d85 src/Pure/ML/exn_debugger.ML
--- 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 []);
diff -r 5c678ee5d34a -r 48c24d0b6d85 src/Pure/ML/exn_properties.ML
--- 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
diff -r 5c678ee5d34a -r 48c24d0b6d85 src/Pure/ML/ml_compiler.ML
--- 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);
diff -r 5c678ee5d34a -r 48c24d0b6d85 src/Pure/ML/ml_compiler0.ML
--- 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;
diff -r 5c678ee5d34a -r 48c24d0b6d85 src/Pure/ML/ml_debugger.ML
--- 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;
diff -r 5c678ee5d34a -r 48c24d0b6d85 src/Pure/Tools/debugger.ML
--- 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];