--- a/src/Pure/General/binding.ML Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/General/binding.ML Thu Sep 12 19:52:01 2024 +0200
@@ -172,7 +172,7 @@
fun pretty (Binding {prefix, qualifier, name, pos, ...}) =
if name = "" then Pretty.str "\"\""
else
- Pretty.markup (Position.markup pos Markup.binding)
+ Pretty.markup (Position.markup_properties pos Markup.binding)
[Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
|> Pretty.quote;
--- a/src/Pure/General/completion.ML Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/General/completion.ML Thu Sep 12 19:52:01 2024 +0200
@@ -61,7 +61,7 @@
fun markup_element completion =
let val {pos, names, ...} = dest completion in
if Position.is_reported pos andalso not (null names) then
- SOME (Position.markup pos Markup.completion, encode completion)
+ SOME (Position.markup_properties pos Markup.completion, encode completion)
else NONE
end;
--- a/src/Pure/General/latex.ML Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/General/latex.ML Thu Sep 12 19:52:01 2024 +0200
@@ -44,7 +44,7 @@
fun text (s, pos) =
if s = "" then []
else if pos = Position.none then [XML.Text s]
- else [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])];
+ else [XML.Elem (Position.markup_properties pos Markup.document_latex, [XML.Text s])];
fun string s = text (s, Position.none);
--- a/src/Pure/General/position.ML Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/General/position.ML Thu Sep 12 19:52:01 2024 +0200
@@ -43,8 +43,8 @@
val def_properties_of: T -> Properties.T
val entity_markup: string -> string * T -> Markup.T
val make_entity_markup: {def: bool} -> serial -> string -> string * T -> Markup.T
- val markup: T -> Markup.T -> Markup.T
- val markup_position: T -> Markup.T
+ val markup_properties: T -> Markup.T -> Markup.T
+ val markup: T -> Markup.T
val is_reported: T -> bool
val is_reported_range: T -> bool
val reported_text: T -> Markup.T -> string -> string
@@ -242,8 +242,8 @@
else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
in Markup.entity kind name |> Markup.properties props end;
-val markup = Markup.properties o properties_of;
-fun markup_position pos = markup pos Markup.position;
+val markup_properties = Markup.properties o properties_of;
+fun markup pos = markup_properties pos Markup.position;
(* reports *)
@@ -252,7 +252,7 @@
fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
fun reported_text pos m txt =
- if is_reported pos then Markup.markup (markup pos m) txt else "";
+ if is_reported pos then Markup.markup (markup_properties pos m) txt else "";
fun report_text pos markup txt =
if Print_Mode.PIDE_enabled () then Output.report [reported_text pos markup txt] else ();
@@ -265,7 +265,7 @@
fun reports_text args =
if Print_Mode.PIDE_enabled () then
Output.report (args |> map (fn ((pos, m), txt) =>
- if is_reported pos then Markup.markup (markup pos m) txt else ""))
+ if is_reported pos then Markup.markup (markup_properties pos m) txt else ""))
else ();
val reports = map (rpair "") #> reports_text;
@@ -290,7 +290,7 @@
fun here pos =
let val (s1, s2) = here_strs pos
- in if s2 = "" then "" else s1 ^ Markup.markup (markup_position pos) s2 end;
+ in if s2 = "" then "" else s1 ^ Markup.markup (markup pos) s2 end;
val here_list = map here #> distinct (op =) #> implode;
--- a/src/Pure/General/pretty.ML Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/General/pretty.ML Thu Sep 12 19:52:01 2024 +0200
@@ -145,8 +145,8 @@
fun mark_str (m, s) = mark m (str s);
fun marks_str (ms, s) = fold_rev mark ms (str s);
-val mark_position = mark o Position.markup_position;
-fun mark_str_position (pos, s) = mark_str (Position.markup_position pos, s);
+val mark_position = mark o Position.markup;
+fun mark_str_position (pos, s) = mark_str (Position.markup pos, s);
val item = markup Markup.item;
val text_fold = markup Markup.text_fold;
--- a/src/Pure/Isar/proof.ML Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/Isar/proof.ML Thu Sep 12 19:52:01 2024 +0200
@@ -394,7 +394,7 @@
else if mode = Backward then Proof_Context.pretty_ctxt ctxt
else [];
- val position_markup = Position.markup_position (Position.thread_data ());
+ val position_markup = Position.markup (Position.thread_data ());
in
[Pretty.block
[Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
--- a/src/Pure/Syntax/term_position.ML Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/Syntax/term_position.ML Thu Sep 12 19:52:01 2024 +0200
@@ -29,7 +29,7 @@
fun pretty pos = Pretty.mark_str_position (pos, position_dummy);
fun encode pos =
- YXML.string_of (XML.Elem (Position.markup_position pos, [position_text]));
+ YXML.string_of (XML.Elem (Position.markup pos, [position_text]));
fun decode str =
(case YXML.parse_body str handle Fail msg => error msg of
--- a/src/Pure/Tools/find_consts.ML Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/Tools/find_consts.ML Thu Sep 12 19:52:01 2024 +0200
@@ -115,7 +115,7 @@
|> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst))
|> map (apsnd fst o snd);
- val position_markup = Position.markup_position (Position.thread_data ());
+ val position_markup = Position.markup (Position.thread_data ());
in
Pretty.block
(Pretty.fbreaks
--- a/src/Pure/Tools/find_theorems.ML Thu Sep 12 19:46:08 2024 +0200
+++ b/src/Pure/Tools/find_theorems.ML Thu Sep 12 19:52:01 2024 +0200
@@ -481,7 +481,7 @@
(if returned < found
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
- val position_markup = Position.markup_position (Position.thread_data ());
+ val position_markup = Position.markup (Position.thread_data ());
in
Pretty.block
(Pretty.fbreaks