# HG changeset patch
# User wenzelm
# Date 1726860849 -7200
# Node ID dbaa780c6d0d9f24325b0dfef3a1480ae62940d1
# Parent  d97fdabd9e2b990954ece27589f7952851ff5c04
more markup elements;

diff -r d97fdabd9e2b -r dbaa780c6d0d 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;