# HG changeset patch
# User wenzelm
# Date 1727604589 -7200
# Node ID c35d7bddbb00655e456310a4a49567271b8300f8
# Parent  71ea31c8ed8552a632d9a36177bfd80f0a20cc4f
more operations;

diff -r 71ea31c8ed85 -r c35d7bddbb00 src/Pure/PIDE/markup.ML
--- 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