# HG changeset patch
# User wenzelm
# Date 1720131152 -7200
# Node ID 7ea69c26524bf80fa3903ac6da4e76b3352d4415
# Parent  d59cc10a6888ea0cd2ed8297d64cd524a10c7c66
tuned signature: more operations;

diff -r d59cc10a6888 -r 7ea69c26524b src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Jul 04 19:16:12 2024 +0200
+++ b/src/Pure/General/pretty.ML	Fri Jul 05 00:12:32 2024 +0200
@@ -195,7 +195,7 @@
 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
 
 val position =
-  enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
+  enum "," "{" "}" o map (str o Properties.print_eq) o Position.properties_of;
 
 fun here pos =
   let
diff -r d59cc10a6888 -r 7ea69c26524b src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Thu Jul 04 19:16:12 2024 +0200
+++ b/src/Pure/General/properties.ML	Fri Jul 05 00:12:32 2024 +0200
@@ -8,6 +8,7 @@
 sig
   type entry = string * string
   type T = entry list
+  val print_eq: entry -> string
   val entry_ord: entry ord
   val ord: T ord
   val defined: T -> string -> bool
@@ -25,8 +26,11 @@
 struct
 
 type entry = string * string;
+
 type T = entry list;
 
+fun print_eq (a, b) = a ^ "=" ^ b;
+
 val entry_ord = prod_ord string_ord string_ord;
 val ord = list_ord entry_ord;
 
diff -r d59cc10a6888 -r 7ea69c26524b src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Thu Jul 04 19:16:12 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Fri Jul 05 00:12:32 2024 +0200
@@ -102,7 +102,7 @@
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
-  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
+  else (XY ^ name ^ implode (map (fn p => Y ^ Properties.print_eq p) atts) ^ X, XYX);
 
 fun output_markup_elem markup =
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))