# HG changeset patch
# User wenzelm
# Date 1726163521 -7200
# Node ID 2e33897071b6e0904fafa8063340151d89478469
# Parent  9af593e9e454729a3a07eaeb41a0df972b5977b7
clarified signature;

diff -r 9af593e9e454 -r 2e33897071b6 src/Pure/General/binding.ML
--- 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;
 
diff -r 9af593e9e454 -r 2e33897071b6 src/Pure/General/completion.ML
--- 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;
 
diff -r 9af593e9e454 -r 2e33897071b6 src/Pure/General/latex.ML
--- 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);
 
diff -r 9af593e9e454 -r 2e33897071b6 src/Pure/General/position.ML
--- 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;
 
diff -r 9af593e9e454 -r 2e33897071b6 src/Pure/General/pretty.ML
--- 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;
diff -r 9af593e9e454 -r 2e33897071b6 src/Pure/Isar/proof.ML
--- 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 ^ ")")]] @
diff -r 9af593e9e454 -r 2e33897071b6 src/Pure/Syntax/term_position.ML
--- 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
diff -r 9af593e9e454 -r 2e33897071b6 src/Pure/Tools/find_consts.ML
--- 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
diff -r 9af593e9e454 -r 2e33897071b6 src/Pure/Tools/find_theorems.ML
--- 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