more operations;

--- a/src/Pure/PIDE/markup.ML	Sun Sep 29 11:18:34 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Sun Sep 29 12:09:49 2024 +0200
@@ -7,6 +7,7 @@
 signature MARKUP =
 sig
   type T = string * Properties.T
+  val ord: T ord
   val empty: T
   val is_empty: T -> bool
   val properties: Properties.T -> T -> T
@@ -298,6 +299,8 @@
 
 type T = string * Properties.T;
 
+val ord = prod_ord string_ord Properties.ord;
+
 val empty = ("", []);
 
 fun is_empty ("", _) = true