# HG changeset patch # User wenzelm # Date 1457182281 -3600 # Node ID 5732f1c31566e85e834bca7a87b3a7b812f43dc1 # Parent e73644de5db87a2947a068f699559bf1139d09a4 tuned signature -- clarified modules; diff -r e73644de5db8 -r 5732f1c31566 src/Pure/Isar/runtime.ML --- 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 diff -r e73644de5db8 -r 5732f1c31566 src/Pure/ML/exn_debugger.ML --- 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 = diff -r e73644de5db8 -r 5732f1c31566 src/Pure/ML/exn_output.ML --- 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; diff -r e73644de5db8 -r 5732f1c31566 src/Pure/ML/exn_properties.ML --- 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 diff -r e73644de5db8 -r 5732f1c31566 src/Pure/ML/ml_compiler.ML --- 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; diff -r e73644de5db8 -r 5732f1c31566 src/Pure/ROOT --- 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" diff -r e73644de5db8 -r 5732f1c31566 src/Pure/ROOT.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"; diff -r e73644de5db8 -r 5732f1c31566 src/Pure/Tools/debugger.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];