tuned signature;
authorwenzelm
Sat Apr 02 21:55:32 2016 +0200 (2016-04-02 ago)
changeset 6282148c24d0b6d85
parent 62820 5c678ee5d34a
child 62822 941b6a48ff67
tuned signature;
src/Pure/General/exn.ML
src/Pure/Isar/runtime.ML
src/Pure/ML/exn_debugger.ML
src/Pure/ML/exn_properties.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler0.ML
src/Pure/ML/ml_debugger.ML
src/Pure/Tools/debugger.ML
     1.1 --- a/src/Pure/General/exn.ML	Sat Apr 02 21:54:51 2016 +0200
     1.2 +++ b/src/Pure/General/exn.ML	Sat Apr 02 21:55:32 2016 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  signature EXN =
     1.5  sig
     1.6    include BASIC_EXN
     1.7 +  val polyml_location: exn -> PolyML.location option
     1.8    val reraise: exn -> 'a
     1.9    datatype 'a result = Res of 'a | Exn of exn
    1.10    val get_res: 'a result -> 'a option
    1.11 @@ -38,12 +39,11 @@
    1.12  structure Exn: EXN =
    1.13  struct
    1.14  
    1.15 -(* reraise *)
    1.16 +(* location *)
    1.17  
    1.18 -fun reraise exn =
    1.19 -  (case PolyML.exceptionLocation exn of
    1.20 -    NONE => raise exn
    1.21 -  | SOME location => PolyML.raiseWithLocation (exn, location));
    1.22 +val polyml_location = PolyML.Exception.exceptionLocation;
    1.23 +
    1.24 +val reraise = PolyML.Exception.reraise;
    1.25  
    1.26  
    1.27  (* user errors *)
     2.1 --- a/src/Pure/Isar/runtime.ML	Sat Apr 02 21:54:51 2016 +0200
     2.2 +++ b/src/Pure/Isar/runtime.ML	Sat Apr 02 21:55:32 2016 +0200
     2.3 @@ -159,7 +159,7 @@
     2.4  local
     2.5  
     2.6  fun print_entry (name, loc) =
     2.7 -  Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_location loc));
     2.8 +  Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_polyml_location loc));
     2.9  
    2.10  fun exception_debugger output e =
    2.11    let
     3.1 --- a/src/Pure/ML/exn_debugger.ML	Sat Apr 02 21:54:51 2016 +0200
     3.2 +++ b/src/Pure/ML/exn_debugger.ML	Sat Apr 02 21:55:32 2016 +0200
     3.3 @@ -6,7 +6,8 @@
     3.4  
     3.5  signature EXN_DEBUGGER =
     3.6  sig
     3.7 -  val capture_exception_trace: (unit -> 'a) -> (string * ML_Debugger.location) list * 'a Exn.result
     3.8 +  val capture_exception_trace:
     3.9 +    (unit -> 'a) -> (string * ML_Compiler0.polyml_location) list * 'a Exn.result
    3.10  end;
    3.11  
    3.12  structure Exn_Debugger: EXN_DEBUGGER =
    3.13 @@ -15,7 +16,8 @@
    3.14  (* thread data *)
    3.15  
    3.16  local
    3.17 -  val tag = Universal.tag () : ((string * ML_Debugger.location) * exn) list option Universal.tag;
    3.18 +  val tag =
    3.19 +    Universal.tag () : ((string * ML_Compiler0.polyml_location) * exn) list option Universal.tag;
    3.20  in
    3.21  
    3.22  fun start_trace () = Thread.setLocal (tag, SOME []);
     4.1 --- a/src/Pure/ML/exn_properties.ML	Sat Apr 02 21:54:51 2016 +0200
     4.2 +++ b/src/Pure/ML/exn_properties.ML	Sat Apr 02 21:55:32 2016 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  signature EXN_PROPERTIES =
     4.6  sig
     4.7 -  val position_of_location: PolyML.location -> Position.T
     4.8 +  val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T
     4.9    val position: exn -> Position.T
    4.10    val get: exn -> Properties.T
    4.11    val update: Properties.entry list -> exn -> exn
    4.12 @@ -17,7 +17,7 @@
    4.13  
    4.14  (* source locations *)
    4.15  
    4.16 -fun props_of_location (loc: PolyML.location) =
    4.17 +fun props_of_polyml_location (loc: ML_Compiler0.polyml_location) =
    4.18    (case YXML.parse_body (#file loc) of
    4.19      [] => []
    4.20    | [XML.Text file] =>
    4.21 @@ -25,25 +25,25 @@
    4.22        else [(Markup.fileN, ML_System.standard_path file)]
    4.23    | body => XML.Decode.properties body);
    4.24  
    4.25 -fun position_of_location loc =
    4.26 +fun position_of_polyml_location loc =
    4.27    Position.make
    4.28     {line = FixedInt.toInt (#startLine loc),
    4.29      offset = FixedInt.toInt (#startPosition loc),
    4.30      end_offset = FixedInt.toInt (#endPosition loc),
    4.31 -    props = props_of_location loc};
    4.32 +    props = props_of_polyml_location loc};
    4.33  
    4.34  fun position exn =
    4.35 -  (case PolyML.exceptionLocation exn of
    4.36 +  (case Exn.polyml_location exn of
    4.37      NONE => Position.none
    4.38 -  | SOME loc => position_of_location loc);
    4.39 +  | SOME loc => position_of_polyml_location loc);
    4.40  
    4.41  
    4.42  (* exception properties *)
    4.43  
    4.44  fun get exn =
    4.45 -  (case PolyML.exceptionLocation exn of
    4.46 +  (case Exn.polyml_location exn of
    4.47      NONE => []
    4.48 -  | SOME loc => props_of_location loc);
    4.49 +  | SOME loc => props_of_polyml_location loc);
    4.50  
    4.51  fun update entries exn =
    4.52    if Exn.is_interrupt exn then exn
    4.53 @@ -51,8 +51,8 @@
    4.54      let
    4.55        val loc =
    4.56          the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
    4.57 -          (PolyML.exceptionLocation exn);
    4.58 -      val props = props_of_location loc;
    4.59 +          (Exn.polyml_location exn);
    4.60 +      val props = props_of_polyml_location loc;
    4.61        val props' = fold Properties.put entries props;
    4.62      in
    4.63        if props = props' then exn
     5.1 --- a/src/Pure/ML/ml_compiler.ML	Sat Apr 02 21:54:51 2016 +0200
     5.2 +++ b/src/Pure/ML/ml_compiler.ML	Sat Apr 02 21:55:32 2016 +0200
     5.3 @@ -38,7 +38,7 @@
     5.4  (* parse trees *)
     5.5  
     5.6  fun breakpoint_position loc =
     5.7 -  let val pos = Position.no_range_position (Exn_Properties.position_of_location loc) in
     5.8 +  let val pos = Position.no_range_position (Exn_Properties.position_of_polyml_location loc) in
     5.9      (case Position.offset_of pos of
    5.10        NONE => pos
    5.11      | SOME 1 => pos
    5.12 @@ -60,7 +60,7 @@
    5.13      (* syntax reports *)
    5.14  
    5.15      fun reported_types loc types =
    5.16 -      let val pos = Exn_Properties.position_of_location loc in
    5.17 +      let val pos = Exn_Properties.position_of_polyml_location loc in
    5.18          is_reported pos ?
    5.19            let
    5.20              val xml =
    5.21 @@ -72,8 +72,8 @@
    5.22  
    5.23      fun reported_entity kind loc decl =
    5.24        let
    5.25 -        val pos = Exn_Properties.position_of_location loc;
    5.26 -        val def_pos = Exn_Properties.position_of_location decl;
    5.27 +        val pos = Exn_Properties.position_of_polyml_location loc;
    5.28 +        val def_pos = Exn_Properties.position_of_polyml_location decl;
    5.29        in
    5.30          (is_reported pos andalso pos <> def_pos) ?
    5.31            let
    5.32 @@ -83,7 +83,7 @@
    5.33        end;
    5.34  
    5.35      fun reported_completions loc names =
    5.36 -      let val pos = Exn_Properties.position_of_location loc in
    5.37 +      let val pos = Exn_Properties.position_of_polyml_location loc in
    5.38          if is_reported pos andalso not (null names) then
    5.39            let
    5.40              val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
    5.41 @@ -189,7 +189,7 @@
    5.42  
    5.43      fun message {message = msg, hard, location = loc, context = _} =
    5.44        let
    5.45 -        val pos = Exn_Properties.position_of_location loc;
    5.46 +        val pos = Exn_Properties.position_of_polyml_location loc;
    5.47          val txt =
    5.48            (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
    5.49            Pretty.string_of (Pretty.from_polyml msg);
     6.1 --- a/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 21:54:51 2016 +0200
     6.2 +++ b/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 21:55:32 2016 +0200
     6.3 @@ -7,6 +7,7 @@
     6.4  
     6.5  signature ML_COMPILER0 =
     6.6  sig
     6.7 +  type polyml_location = PolyML.location
     6.8    type context =
     6.9     {name_space: ML_Name_Space.T,
    6.10      print_depth: int option,
    6.11 @@ -24,6 +25,9 @@
    6.12  structure ML_Compiler0: ML_COMPILER0 =
    6.13  struct
    6.14  
    6.15 +type polyml_location = PolyML.location;
    6.16 +
    6.17 +
    6.18  (* global options *)
    6.19  
    6.20  val _ = PolyML.Compiler.reportUnreferencedIds := true;
     7.1 --- a/src/Pure/ML/ml_debugger.ML	Sat Apr 02 21:54:51 2016 +0200
     7.2 +++ b/src/Pure/ML/ml_debugger.ML	Sat Apr 02 21:55:32 2016 +0200
     7.3 @@ -10,17 +10,16 @@
     7.4    val exn_id: exn -> exn_id
     7.5    val print_exn_id: exn_id -> string
     7.6    val eq_exn_id: exn_id * exn_id -> bool
     7.7 -  type location
     7.8 -  val on_entry: (string * location -> unit) option -> unit
     7.9 -  val on_exit: (string * location -> unit) option -> unit
    7.10 -  val on_exit_exception: (string * location -> exn -> unit) option -> unit
    7.11 -  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
    7.12 +  val on_entry: (string * ML_Compiler0.polyml_location -> unit) option -> unit
    7.13 +  val on_exit: (string * ML_Compiler0.polyml_location -> unit) option -> unit
    7.14 +  val on_exit_exception: (string * ML_Compiler0.polyml_location -> exn -> unit) option -> unit
    7.15 +  val on_breakpoint: (ML_Compiler0.polyml_location * bool Unsynchronized.ref -> unit) option -> unit
    7.16    type state
    7.17    val state: Thread.thread -> state list
    7.18    val debug_function: state -> string
    7.19    val debug_function_arg: state -> ML_Name_Space.valueVal
    7.20    val debug_function_result: state -> ML_Name_Space.valueVal
    7.21 -  val debug_location: state -> location
    7.22 +  val debug_location: state -> ML_Compiler0.polyml_location
    7.23    val debug_name_space: state -> ML_Name_Space.T
    7.24    val debug_local_name_space: state -> ML_Name_Space.T
    7.25  end;
    7.26 @@ -49,8 +48,6 @@
    7.27  
    7.28  (* hooks *)
    7.29  
    7.30 -type location = PolyML.location;
    7.31 -
    7.32  val on_entry = PolyML.DebuggerInterface.setOnEntry;
    7.33  val on_exit = PolyML.DebuggerInterface.setOnExit;
    7.34  val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
     8.1 --- a/src/Pure/Tools/debugger.ML	Sat Apr 02 21:54:51 2016 +0200
     8.2 +++ b/src/Pure/Tools/debugger.ML	Sat Apr 02 21:55:32 2016 +0200
     8.3 @@ -209,7 +209,8 @@
     8.4    Output.protocol_message (Markup.debugger_state thread_name)
     8.5     [get_debugging ()
     8.6      |> map (fn st =>
     8.7 -      (Position.properties_of (Exn_Properties.position_of_location (ML_Debugger.debug_location st)),
     8.8 +      (Position.properties_of
     8.9 +        (Exn_Properties.position_of_polyml_location (ML_Debugger.debug_location st)),
    8.10         ML_Debugger.debug_function st))
    8.11      |> let open XML.Encode in list (pair properties string) end
    8.12      |> YXML.string_of_body];