# HG changeset patch
# User wenzelm
# Date 1726848544 -7200
# Node ID b2eaa342aae52d691bb4b45e1477c040efd906bd
# Parent  8ad5e6df050bf3f7c476aaa21ec4c16d50d18d7a
support more markup elements;

diff -r 8ad5e6df050b -r b2eaa342aae5 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Sep 20 15:35:16 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Sep 20 18:09:04 2024 +0200
@@ -68,6 +68,8 @@
   val position_property: Properties.entry -> bool
   val def_name: string -> string
   val notation_mixfixN: string
+  val notation_prefixN: string
+  val notation_postfixN: string
   val notation_infixN: string
   val notation_binderN: string
   val notations: string list
@@ -443,9 +445,12 @@
 (* notation: mixfix annotations *)
 
 val notation_mixfixN = "mixfix";
+val notation_prefixN = "prefix";
+val notation_postfixN = "postfix";
 val notation_infixN = "infix";
 val notation_binderN = "binder";
-val notations = [notation_mixfixN, notation_infixN, notation_binderN];
+val notations =
+  [notation_mixfixN, notation_prefixN, notation_postfixN, notation_infixN, notation_binderN];
 
 val notationN = "notation";
 fun notation {kind, name} = (notationN, kind_proper kind @ name_proper name);
diff -r 8ad5e6df050b -r b2eaa342aae5 src/Pure/PIDE/markup_expression.ML
--- a/src/Pure/PIDE/markup_expression.ML	Fri Sep 20 15:35:16 2024 +0200
+++ b/src/Pure/PIDE/markup_expression.ML	Fri Sep 20 18:09:04 2024 +0200
@@ -10,6 +10,12 @@
   val setup_kind: binding -> theory -> string * theory
   val check: Proof.context -> xstring * Position.T -> Markup.T
   val setup: binding -> Markup.T
+  val markup_type: Markup.T
+  val markup_type_application: Markup.T
+  val markup_term: Markup.T
+  val markup_term_application: Markup.T
+  val markup_prop: Markup.T
+  val markup_prop_application: Markup.T
 end;
 
 structure Markup_Expression: MARKUP_EXPRESSION =
@@ -44,4 +50,16 @@
 fun setup binding =
   Context.>>> (Context.map_theory_result (setup_kind binding #>> Markup.expression));
 
+
+(* concrete markup *)
+
+val markup_type = setup (Binding.make ("type", \<^here>));
+val markup_type_application = setup (Binding.make ("type_application", \<^here>));
+
+val markup_term = setup (Binding.make ("term", \<^here>));
+val markup_term_application = setup (Binding.make ("term_application", \<^here>));
+
+val markup_prop = setup (Binding.make ("prop", \<^here>));
+val markup_prop_application = setup (Binding.make ("prop_application", \<^here>));
+
 end;