more markup elements;
authorwenzelm
Fri, 20 Sep 2024 21:34:09 +0200
changeset 80915 dbaa780c6d0d
parent 80914 d97fdabd9e2b
child 80916 01b8c8d17f13
more markup elements;
src/Pure/PIDE/markup_expression.ML
--- a/src/Pure/PIDE/markup_expression.ML	Fri Sep 20 19:51:08 2024 +0200
+++ b/src/Pure/PIDE/markup_expression.ML	Fri Sep 20 21:34:09 2024 +0200
@@ -14,8 +14,10 @@
   val markup_type_application: Markup.T
   val markup_term: Markup.T
   val markup_term_application: Markup.T
+  val markup_term_abstraction: Markup.T
   val markup_prop: Markup.T
   val markup_prop_application: Markup.T
+  val markup_prop_abstraction: Markup.T
 end;
 
 structure Markup_Expression: MARKUP_EXPRESSION =
@@ -58,8 +60,10 @@
 
 val markup_term = setup (Binding.make ("term", \<^here>));
 val markup_term_application = setup (Binding.make ("term_application", \<^here>));
+val markup_term_abstraction = setup (Binding.make ("term_abstraction", \<^here>));
 
 val markup_prop = setup (Binding.make ("prop", \<^here>));
 val markup_prop_application = setup (Binding.make ("prop_application", \<^here>));
+val markup_prop_abstraction = setup (Binding.make ("prop_abstraction", \<^here>));
 
 end;