--- a/src/Pure/PIDE/markup.ML Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Dec 07 23:50:18 2024 +0100
@@ -196,6 +196,8 @@
val comment1N: string val comment1: T
val comment2N: string val comment2: T
val comment3N: string val comment3: T
+ val syntaxN: string val syntax_properties: bool -> T -> T
+ val has_syntax: Properties.T -> bool
val elapsedN: string
val cpuN: string
val gcN: string
@@ -675,6 +677,19 @@
val (comment3N, comment3) = markup_elem "comment3";
+(* concrete syntax (notably mixfix notation) *)
+
+val syntaxN = "syntax";
+
+val syntax_elements = [improperN, freeN, skolemN];
+
+fun syntax_properties syntax (m as (elem, props): T) =
+ if syntax andalso member (op =) syntax_elements elem
+ then (elem, Properties.put (syntaxN, "true") props) else m;
+
+fun has_syntax props = Properties.get_bool props syntaxN;
+
+
(* timing *)
val elapsedN = "elapsed";