diff -r 0c898f7d9b15 -r 9e2eb05cc2b7 src/Pure/PIDE/markup_kind.ML --- a/src/Pure/PIDE/markup_kind.ML Sat Oct 05 15:18:49 2024 +0200 +++ b/src/Pure/PIDE/markup_kind.ML Sat Oct 05 22:24:24 2024 +0200 @@ -22,6 +22,7 @@ val markup_postfix: Markup.T val markup_infix: Markup.T val markup_binder: Markup.T + val markup_literal: Markup.T val markup_type_application: Markup.T val markup_application: Markup.T val markup_abstraction: Markup.T @@ -100,6 +101,7 @@ val markup_postfix = setup_notation (Binding.make ("postfix", \<^here>)); val markup_infix = setup_notation (Binding.make ("infix", \<^here>)); val markup_binder = setup_notation (Binding.make ("binder", \<^here>)); +val markup_literal = setup_notation (Binding.make ("literal", \<^here>)); val markup_type_application = setup_notation (Binding.make ("type_application", \<^here>)); val markup_application = setup_notation (Binding.make ("application", \<^here>));