--- a/src/HOL/Library/Pattern_Aliases.thy Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Library/Pattern_Aliases.thy Fri Sep 06 20:31:20 2024 +0200
@@ -200,7 +200,7 @@
@{thm test_2.simps(1)}
|> Thm.prop_of
|> Syntax.string_of_term \<^context>
- |> YXML.content_of
+ |> Protocol_Message.clean_output
val expected = "test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'"
in \<^assert> (actual = expected) end
\<close>
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Sep 06 20:31:20 2024 +0200
@@ -422,7 +422,7 @@
(*^ "\n" ^ string_of_reports reports*)
in
"mutant of " ^ Thm_Name.short thm_name ^ ":\n" ^
- YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^
+ Protocol_Message.clean_output (Syntax.string_of_term_global thy t) ^ "\n" ^
space_implode "; " (map string_of_mtd_result results)
end
--- a/src/HOL/Tools/ATP/atp_util.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Fri Sep 06 20:31:20 2024 +0200
@@ -143,7 +143,7 @@
val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
fun maybe_quote ctxt y =
let
- val s = YXML.content_of y
+ val s = Protocol_Message.clean_output y
val is_literal = Keyword.is_literal (Thy_Header.get_keywords' ctxt)
val q = if Config.get ctxt proof_cartouches then cartouche else quote
in
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Sep 06 20:31:20 2024 +0200
@@ -318,7 +318,7 @@
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
fun quot_normal_name_for_type ctxt T =
- quot_normal_prefix ^ YXML.content_of (Syntax.string_of_typ ctxt T)
+ quot_normal_prefix ^ Protocol_Message.clean_output (Syntax.string_of_typ ctxt T)
val strip_first_name_sep =
Substring.full #> Substring.position name_sep ##> Substring.triml 1
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Sep 06 20:31:20 2024 +0200
@@ -303,7 +303,7 @@
fun bound_comment ctxt debug nick T R =
short_name nick ^
- (if debug then " :: " ^ YXML.content_of (Syntax.string_of_typ ctxt T) else "") ^
+ (if debug then " :: " ^ Protocol_Message.clean_output (Syntax.string_of_typ ctxt T) else "") ^
" : " ^ string_for_rep R
fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Sep 06 20:31:20 2024 +0200
@@ -162,7 +162,7 @@
fun nth_name j =
(case xref of
- Facts.Fact s => cartouche (simplify_spaces (YXML.content_of s)) ^ bracket
+ Facts.Fact s => cartouche (simplify_spaces (Protocol_Message.clean_output s)) ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
| Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
| Facts.Named ((name, _), SOME intervals) =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Sep 06 20:31:20 2024 +0200
@@ -165,7 +165,7 @@
expect : string}
fun string_of_params (params : params) =
- YXML.content_of (ML_Pretty.string_of (ML_system_pretty (params, 100)))
+ Protocol_Message.clean_output (ML_Pretty.string_of (ML_system_pretty (params, 100)))
fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
induction_rules = Exclude ?
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Sep 06 20:31:20 2024 +0200
@@ -132,7 +132,7 @@
fun hackish_string_of_term ctxt =
(* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
#> *) Print_Mode.setmp [] (Syntax.string_of_term ctxt)
- #> YXML.content_of
+ #> Protocol_Message.clean_output
#> simplify_spaces
val spying_version = "d"
--- a/src/Pure/PIDE/protocol_message.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/Pure/PIDE/protocol_message.ML Fri Sep 06 20:31:20 2024 +0200
@@ -10,6 +10,7 @@
val marker: string -> Properties.T -> unit
val command_positions: string -> XML.body -> XML.body
val command_positions_yxml: string -> string -> string
+ val clean_output: string -> string
end;
structure Protocol_Message: PROTOCOL_MESSAGE =
@@ -37,4 +38,16 @@
fun command_positions_yxml id =
YXML.string_of_body o command_positions id o YXML.parse_body;
+
+(* clean output *)
+
+fun clean_output msg =
+ (case try YXML.parse_body msg of
+ SOME xml =>
+ xml |> XML.filter_elements
+ {remove = fn a => a = Markup.reportN,
+ expose = fn a => a = Markup.no_reportN}
+ |> XML.content_of
+ | NONE => msg);
+
end;
--- a/src/Pure/PIDE/xml.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/Pure/PIDE/xml.ML Fri Sep 06 20:31:20 2024 +0200
@@ -39,6 +39,7 @@
val enclose: string -> string -> body -> body
val add_content: tree -> Buffer.T -> Buffer.T
val trim_blanks: body -> body
+ val filter_elements: {remove: string -> bool, expose: string -> bool} -> body -> body
val header: string
val text: string -> string
val element: string -> attributes -> string list -> string
@@ -111,6 +112,26 @@
| Text s => s |> raw_explode |> trim Symbol.is_blank |> implode |> string);
+(* filter markup elements *)
+
+fun filter_elements {remove, expose} =
+ let
+ fun filter ts =
+ ts |> maps (fn t =>
+ (case XML.unwrap_elem t of
+ SOME ((markup, body1), body2) =>
+ if remove (#1 markup) then []
+ else if expose (#1 markup) then filter body2
+ else [XML.wrap_elem ((markup, body1), filter body2)]
+ | NONE =>
+ (case t of
+ XML.Elem (markup, body) =>
+ if remove (#1 markup) then []
+ else if expose (#1 markup) then filter body
+ else [XML.Elem (markup, filter body)]
+ | _ => [t])));
+ in filter end;
+
(** string representation **)
--- a/src/Pure/PIDE/yxml.ML Fri Sep 06 19:17:29 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML Fri Sep 06 20:31:20 2024 +0200
@@ -33,7 +33,6 @@
val parse_body_bytes: Bytes.T -> XML.body
val parse: string -> XML.tree
val parse_bytes: Bytes.T -> XML.tree
- val content_of: string -> string
val is_wellformed: string -> bool
end;
@@ -170,8 +169,6 @@
end;
-val content_of = parse_body #> XML.content_of;
-
fun is_wellformed s = string_of_body (parse_body s) = s
handle Fail _ => false;