# HG changeset patch
# User wenzelm
# Date 1726146547 -7200
# Node ID e71cb37c7395d2b44ea02c8910342db4419c96d9
# Parent  320bcbf34849433a1a506150c45213d131c695ff
clarified signature: more explicit operations;

diff -r 320bcbf34849 -r e71cb37c7395 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Thu Sep 12 14:42:04 2024 +0200
+++ b/src/Pure/General/position.ML	Thu Sep 12 15:09:07 2024 +0200
@@ -44,6 +44,7 @@
   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 is_reported: T -> bool
   val is_reported_range: T -> bool
   val reported_text: T -> Markup.T -> string -> string
@@ -242,6 +243,7 @@
   in Markup.entity kind name |> Markup.properties props end;
 
 val markup = Markup.properties o properties_of;
+fun markup_position pos = markup pos Markup.position;
 
 
 (* reports *)
@@ -287,13 +289,8 @@
   | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
 
 fun here pos =
-  let
-    val props = properties_of pos;
-    val (s1, s2) = here_strs pos;
-  in
-    if s2 = "" then ""
-    else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
-  end;
+  let val (s1, s2) = here_strs pos
+  in if s2 = "" then "" else s1 ^ Markup.markup (markup_position pos) s2 end;
 
 val here_list = map here #> distinct (op =) #> implode;
 
diff -r 320bcbf34849 -r e71cb37c7395 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Sep 12 14:42:04 2024 +0200
+++ b/src/Pure/General/pretty.ML	Thu Sep 12 15:09:07 2024 +0200
@@ -41,6 +41,8 @@
   val mark: Markup.T -> T -> T
   val mark_str: Markup.T * string -> T
   val marks_str: Markup.T list * string -> T
+  val mark_position: Position.T -> T -> T
+  val mark_str_position: Position.T * string -> T
   val item: T list -> T
   val text_fold: T list -> T
   val keyword1: string -> T
@@ -139,9 +141,13 @@
 
 fun markup m = markup_block {markup = m, consistent = false, indent = 0};
 fun mark m prt = if m = Markup.empty then prt else markup m [prt];
+
 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 item = markup Markup.item;
 val text_fold = markup Markup.text_fold;
 
@@ -169,13 +175,8 @@
   enum "," "{" "}" o map (str o Properties.print_eq) o Position.properties_of;
 
 fun here pos =
-  let
-    val props = Position.properties_of pos;
-    val (s1, s2) = Position.here_strs pos;
-  in
-    if s2 = "" then []
-    else [str s1, mark_str (Markup.properties props Markup.position, s2)]
-  end;
+  let val (s1, s2) = Position.here_strs pos
+  in if s2 = "" then [] else [str s1, mark_str_position (pos, s2)] end;
 
 val list = enum ",";
 fun str_list lpar rpar strs = list lpar rpar (map str strs);
diff -r 320bcbf34849 -r e71cb37c7395 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Sep 12 14:42:04 2024 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Sep 12 15:09:07 2024 +0200
@@ -394,7 +394,7 @@
       else if mode = Backward then Proof_Context.pretty_ctxt ctxt
       else [];
 
-    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
+    val position_markup = Position.markup_position (Position.thread_data ());
   in
     [Pretty.block
       [Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
diff -r 320bcbf34849 -r e71cb37c7395 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Thu Sep 12 14:42:04 2024 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Sep 12 15:09:07 2024 +0200
@@ -293,8 +293,6 @@
 
 (* results *)
 
-fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
-
 val interactive =
   Config.declare_bool ("interactive", \<^here>) (K false);
 
@@ -308,9 +306,9 @@
 
 local
 
-fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
+fun pretty_fact_name pos (kind, "") = Pretty.mark_position pos (Pretty.keyword1 kind)
   | pretty_fact_name pos (kind, name) =
-      Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1,
+      Pretty.block [Pretty.mark_position pos (Pretty.keyword1 kind), Pretty.brk 1,
         Pretty.str (Long_Name.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
@@ -324,7 +322,7 @@
     if kind = "" orelse no_print interactive ctxt then ()
     else if name = "" then
       print
-        (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
+        (Pretty.block (Pretty.mark_position pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
           pretty_facts ctxt facts))
     else
       print
@@ -352,7 +350,7 @@
 
 fun pretty_vars pos ctxt kind vs =
   Pretty.block
-    (Pretty.fbreaks (position_markup pos (Pretty.mark_str kind) :: map (pretty_var ctxt) vs));
+    (Pretty.fbreaks (Pretty.mark_position pos (Pretty.mark_str kind) :: map (pretty_var ctxt) vs));
 
 val fixes = (Markup.keyword2, "fixes");
 val consts = (Markup.keyword1, "consts");
diff -r 320bcbf34849 -r e71cb37c7395 src/Pure/Syntax/term_position.ML
--- a/src/Pure/Syntax/term_position.ML	Thu Sep 12 14:42:04 2024 +0200
+++ b/src/Pure/Syntax/term_position.ML	Thu Sep 12 15:09:07 2024 +0200
@@ -26,11 +26,10 @@
 val position_dummy = "<position>";
 val position_text = XML.Text position_dummy;
 
-fun pretty pos =
-  Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
+fun pretty pos = Pretty.mark_str_position (pos, position_dummy);
 
 fun encode pos =
-  YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
+  YXML.string_of (XML.Elem (Position.markup_position pos, [position_text]));
 
 fun decode str =
   (case YXML.parse_body str handle Fail msg => error msg of
diff -r 320bcbf34849 -r e71cb37c7395 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Thu Sep 12 14:42:04 2024 +0200
+++ b/src/Pure/Tools/find_consts.ML	Thu Sep 12 15:09:07 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.thread_data ()) Markup.position;
+    val position_markup = Position.markup_position (Position.thread_data ());
   in
     Pretty.block
       (Pretty.fbreaks
diff -r 320bcbf34849 -r e71cb37c7395 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Sep 12 14:42:04 2024 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu Sep 12 15:09:07 2024 +0200
@@ -481,7 +481,7 @@
             (if returned < found
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
-    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
+    val position_markup = Position.markup_position (Position.thread_data ());
   in
     Pretty.block
       (Pretty.fbreaks