# HG changeset patch
# User wenzelm
# Date 1726771099 -7200
# Node ID ac1e8686e523b5a2c94111380a2c4ccb4e3a86fd
# Parent  f4d519d088afb745efe6fb69eba8c8b643d8058f
more operations;

diff -r f4d519d088af -r ac1e8686e523 src/Pure/PIDE/markup_expression.ML
--- a/src/Pure/PIDE/markup_expression.ML	Thu Sep 19 12:41:02 2024 +0200
+++ b/src/Pure/PIDE/markup_expression.ML	Thu Sep 19 20:38:19 2024 +0200
@@ -8,6 +8,7 @@
 sig
   val check_kind: Proof.context -> xstring * Position.T -> string
   val setup_kind: binding -> theory -> string * theory
+  val check: Proof.context -> xstring * Position.T -> Markup.T
   val setup: binding -> Markup.T
 end;
 
@@ -23,6 +24,9 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
+
+(* kind *)
+
 fun check_kind ctxt =
   Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt)) #> #1;
 
@@ -32,6 +36,11 @@
     val (name, data') = Name_Space.define context true (binding, ()) (Data.get thy);
   in (name, Data.put data' thy) end;
 
+
+(* markup *)
+
+fun check ctxt = check_kind ctxt #> Markup.expression;
+
 fun setup binding =
   Context.>>> (Context.map_theory_result (setup_kind binding #>> Markup.expression));