diff -r c5ea0cb4dd91 -r 510f6cb6721e src/Pure/PIDE/markup_expression.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup_expression.ML	Mon Sep 16 19:58:28 2024 +0200
@@ -0,0 +1,38 @@
+(*  Title:      Pure/markup_expression.ML
+    Author:     Makarius
+
+Formally defined kind for Markup.expression.
+*)
+
+signature MARKUP_EXPRESSION =
+sig
+  val check_kind: Proof.context -> xstring * Position.T -> string
+  val setup_kind: binding -> theory -> string * theory
+  val setup: binding -> Markup.T
+end;
+
+structure Markup_Expression: MARKUP_EXPRESSION =
+struct
+
+(* theory data *)
+
+structure Data = Theory_Data
+(
+  type T = unit Name_Space.table;
+  val empty : T = Name_Space.empty_table "markup_expression_kind";
+  fun merge data : T = Name_Space.merge_tables data;
+);
+
+fun check_kind ctxt =
+  Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt)) #> #1;
+
+fun setup_kind binding thy =
+  let
+    val context = Name_Space.map_naming (K Name_Space.global_naming) (Context.Theory thy);
+    val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy);
+  in (name, Data.put data' thy) end;
+
+fun setup binding =
+  Context.>>> (Context.map_theory_result (setup_kind binding #>> Markup.expression));
+
+end;