tuned signature -- clarified modules;
authorwenzelm
Sat Mar 05 13:51:21 2016 +0100 (2016-03-05)
changeset 625165732f1c31566
parent 62515 e73644de5db8
child 62517 091fdc002a52
tuned signature -- clarified modules;
src/Pure/Isar/runtime.ML
src/Pure/ML/exn_debugger.ML
src/Pure/ML/exn_output.ML
src/Pure/ML/exn_properties.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/debugger.ML
     1.1 --- a/src/Pure/Isar/runtime.ML	Sat Mar 05 13:25:41 2016 +0100
     1.2 +++ b/src/Pure/Isar/runtime.ML	Sat Mar 05 13:51:21 2016 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4    exception UNDEF
     1.5    exception EXCURSION_FAIL of exn * string
     1.6    exception TOPLEVEL_ERROR
     1.7 +  val pretty_exn: exn -> Pretty.T
     1.8    val exn_context: Proof.context option -> exn -> exn
     1.9    val thread_context: exn -> exn
    1.10    type error = ((serial * string) * string option)
    1.11 @@ -37,6 +38,14 @@
    1.12  exception TOPLEVEL_ERROR;
    1.13  
    1.14  
    1.15 +(* pretty *)
    1.16 +
    1.17 +fun pretty_exn (exn: exn) =
    1.18 +  Pretty.from_ML
    1.19 +    (ML_Pretty.from_polyml
    1.20 +      (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
    1.21 +
    1.22 +
    1.23  (* exn_context *)
    1.24  
    1.25  exception CONTEXT of Proof.context * exn;
    1.26 @@ -85,7 +94,7 @@
    1.27  fun exn_messages_ids e =
    1.28    let
    1.29      fun raised exn name msgs =
    1.30 -      let val pos = Position.here (Exn_Output.position exn) in
    1.31 +      let val pos = Position.here (Exn_Properties.position exn) in
    1.32          (case msgs of
    1.33            [] => "exception " ^ name ^ " raised" ^ pos
    1.34          | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
    1.35 @@ -123,7 +132,7 @@
    1.36              | THM (msg, i, thms) =>
    1.37                  raised exn ("THM " ^ string_of_int i)
    1.38                    (msg :: robust_context context Thm.string_of_thm thms)
    1.39 -            | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
    1.40 +            | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
    1.41          in [((i, msg), id)] end)
    1.42        and sorted_msgs context exn =
    1.43          sort_distinct (int_ord o apply2 (fst o fst)) (maps exn_msgs (flatten context exn));
    1.44 @@ -150,7 +159,7 @@
    1.45  local
    1.46  
    1.47  fun print_entry (name, loc) =
    1.48 -  Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of loc));
    1.49 +  Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of_location loc));
    1.50  
    1.51  fun exception_debugger output e =
    1.52    let
     2.1 --- a/src/Pure/ML/exn_debugger.ML	Sat Mar 05 13:25:41 2016 +0100
     2.2 +++ b/src/Pure/ML/exn_debugger.ML	Sat Mar 05 13:51:21 2016 +0100
     2.3 @@ -40,7 +40,7 @@
     2.4  
     2.5  local
     2.6    fun eq_exn exns =
     2.7 -    op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Output.position exns);
     2.8 +    op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Properties.position exns);
     2.9  in
    2.10  
    2.11  fun capture_exception_trace e =
     3.1 --- a/src/Pure/ML/exn_output.ML	Sat Mar 05 13:25:41 2016 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,26 +0,0 @@
     3.4 -(*  Title:      Pure/ML/exn_output.ML
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Auxiliary operations for exception output.
     3.8 -*)
     3.9 -
    3.10 -signature EXN_OUTPUT =
    3.11 -sig
    3.12 -  val position: exn -> Position.T
    3.13 -  val pretty: exn -> Pretty.T
    3.14 -end;
    3.15 -
    3.16 -structure Exn_Output: EXN_OUTPUT =
    3.17 -struct
    3.18 -
    3.19 -fun position exn =
    3.20 -  (case PolyML.exceptionLocation exn of
    3.21 -    NONE => Position.none
    3.22 -  | SOME loc => Exn_Properties.position_of loc);
    3.23 -
    3.24 -fun pretty (exn: exn) =
    3.25 -  Pretty.from_ML
    3.26 -    (ML_Pretty.from_polyml
    3.27 -      (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
    3.28 -
    3.29 -end;
     4.1 --- a/src/Pure/ML/exn_properties.ML	Sat Mar 05 13:25:41 2016 +0100
     4.2 +++ b/src/Pure/ML/exn_properties.ML	Sat Mar 05 13:51:21 2016 +0100
     4.3 @@ -6,7 +6,8 @@
     4.4  
     4.5  signature EXN_PROPERTIES =
     4.6  sig
     4.7 -  val position_of: PolyML.location -> Position.T
     4.8 +  val position_of_location: 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  end;
    4.13 @@ -16,7 +17,7 @@
    4.14  
    4.15  (* source locations *)
    4.16  
    4.17 -fun props_of (loc: PolyML.location) =
    4.18 +fun props_of_location (loc: PolyML.location) =
    4.19    (case YXML.parse_body (#file loc) of
    4.20      [] => []
    4.21    | [XML.Text file] =>
    4.22 @@ -24,12 +25,17 @@
    4.23        else [(Markup.fileN, ML_System.standard_path file)]
    4.24    | body => XML.Decode.properties body);
    4.25  
    4.26 -fun position_of loc =
    4.27 +fun position_of_location loc =
    4.28    Position.make
    4.29     {line = FixedInt.toInt (#startLine loc),
    4.30      offset = FixedInt.toInt (#startPosition loc),
    4.31      end_offset = FixedInt.toInt (#endPosition loc),
    4.32 -    props = props_of loc};
    4.33 +    props = props_of_location loc};
    4.34 +
    4.35 +fun position exn =
    4.36 +  (case PolyML.exceptionLocation exn of
    4.37 +    NONE => Position.none
    4.38 +  | SOME loc => position_of_location loc);
    4.39  
    4.40  
    4.41  (* exception properties *)
    4.42 @@ -37,14 +43,14 @@
    4.43  fun get exn =
    4.44    (case PolyML.exceptionLocation exn of
    4.45      NONE => []
    4.46 -  | SOME loc => props_of loc);
    4.47 +  | SOME loc => props_of_location loc);
    4.48  
    4.49  fun update entries exn =
    4.50    let
    4.51      val loc =
    4.52        the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
    4.53          (PolyML.exceptionLocation exn);
    4.54 -    val props = props_of loc;
    4.55 +    val props = props_of_location loc;
    4.56      val props' = fold Properties.put entries props;
    4.57    in
    4.58      if props = props' then exn
     5.1 --- a/src/Pure/ML/ml_compiler.ML	Sat Mar 05 13:25:41 2016 +0100
     5.2 +++ b/src/Pure/ML/ml_compiler.ML	Sat Mar 05 13:51:21 2016 +0100
     5.3 @@ -38,7 +38,7 @@
     5.4  (* parse trees *)
     5.5  
     5.6  fun breakpoint_position loc =
     5.7 -  let val pos = Position.reset_range (Exn_Properties.position_of loc) in
     5.8 +  let val pos = Position.reset_range (Exn_Properties.position_of_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 loc in
    5.17 +      let val pos = Exn_Properties.position_of_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 loc;
    5.26 -        val def_pos = Exn_Properties.position_of decl;
    5.27 +        val pos = Exn_Properties.position_of_location loc;
    5.28 +        val def_pos = Exn_Properties.position_of_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 loc in
    5.37 +      let val pos = Exn_Properties.position_of_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 @@ -190,7 +190,7 @@
    5.42  
    5.43      fun message {message = msg, hard, location = loc, context = _} =
    5.44        let
    5.45 -        val pos = Exn_Properties.position_of loc;
    5.46 +        val pos = Exn_Properties.position_of_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_ML (ML_Pretty.from_polyml msg));
    5.50 @@ -275,7 +275,7 @@
    5.51                (case exn of
    5.52                  STATIC_ERRORS () => ""
    5.53                | Runtime.TOPLEVEL_ERROR => ""
    5.54 -              | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
    5.55 +              | _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised");
    5.56              val _ = output_warnings ();
    5.57              val _ = output_writeln ();
    5.58            in raise_error exn_msg end;
     6.1 --- a/src/Pure/ROOT	Sat Mar 05 13:25:41 2016 +0100
     6.2 +++ b/src/Pure/ROOT	Sat Mar 05 13:51:21 2016 +0100
     6.3 @@ -101,7 +101,6 @@
     6.4      "Isar/toplevel.ML"
     6.5      "Isar/typedecl.ML"
     6.6      "ML/exn_debugger.ML"
     6.7 -    "ML/exn_output.ML"
     6.8      "ML/exn_properties.ML"
     6.9      "ML/fixed_int_dummy.ML"
    6.10      "ML/install_pp_polyml.ML"
     7.1 --- a/src/Pure/ROOT.ML	Sat Mar 05 13:25:41 2016 +0100
     7.2 +++ b/src/Pure/ROOT.ML	Sat Mar 05 13:51:21 2016 +0100
     7.3 @@ -276,7 +276,6 @@
     7.4  use "ML/ml_syntax.ML";
     7.5  use "ML/ml_env.ML";
     7.6  use "ML/ml_options.ML";
     7.7 -use "ML/exn_output.ML";
     7.8  use_no_debug "ML/exn_debugger.ML";
     7.9  use "ML/ml_options.ML";
    7.10  use_no_debug "Isar/runtime.ML";
     8.1 --- a/src/Pure/Tools/debugger.ML	Sat Mar 05 13:25:41 2016 +0100
     8.2 +++ b/src/Pure/Tools/debugger.ML	Sat Mar 05 13:51:21 2016 +0100
     8.3 @@ -210,7 +210,7 @@
     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 (ML_Debugger.debug_location st)),
     8.8 +      (Position.properties_of (Exn_Properties.position_of_location (ML_Debugger.debug_location st)),
     8.9         ML_Debugger.debug_function st))
    8.10      |> let open XML.Encode in list (pair properties string) end
    8.11      |> YXML.string_of_body];