# HG changeset patch # User wenzelm # Date 1733856467 -3600 # Node ID a180b070d4f8d6077f14a9ef9b00981843da7b74 # Parent af49ce611685657e51ba81ab8ad170065173c461 tuned markup; diff -r af49ce611685 -r a180b070d4f8 src/Pure/PIDE/markup_kind.ML --- a/src/Pure/PIDE/markup_kind.ML Tue Dec 10 19:23:55 2024 +0100 +++ b/src/Pure/PIDE/markup_kind.ML Tue Dec 10 19:47:47 2024 +0100 @@ -25,6 +25,7 @@ val markup_pattern: Markup.T val markup_type_literal: Markup.T val markup_literal: Markup.T + val markup_index: Markup.T val markup_type_application: Markup.T val markup_application: Markup.T val markup_abstraction: Markup.T @@ -106,6 +107,7 @@ val markup_pattern = setup_notation (Binding.make ("pattern", \<^here>)); val markup_type_literal = setup_notation (Binding.make ("type_literal", \<^here>)); val markup_literal = setup_notation (Binding.make ("literal", \<^here>)); +val markup_index = setup_notation (Binding.make ("index", \<^here>)); val markup_type_application = setup_notation (Binding.make ("type_application", \<^here>)); val markup_application = setup_notation (Binding.make ("application", \<^here>)); diff -r af49ce611685 -r a180b070d4f8 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Dec 10 19:23:55 2024 +0100 +++ b/src/Pure/pure_thy.ML Tue Dec 10 19:47:47 2024 +0100 @@ -172,8 +172,7 @@ ("_position", typ "float_token \ float_position", Mixfix.mixfix "_"), ("_constify", typ "num_position \ num_const", Mixfix.mixfix "_"), ("_constify", typ "float_position \ float_const", Mixfix.mixfix "_"), - ("_index", typ "logic \ index", - Mixfix.mixfix "(\unbreakable notation=\mixfix index\\\<^bsub>_\<^esub>)"), + ("_index", typ "logic \ index", Mixfix.mixfix "(\unbreakable notation=\index\\\<^bsub>_\<^esub>)"), ("_indexdefault", typ "index", Mixfix.mixfix ""), ("_indexvar", typ "index", Mixfix.mixfix "'\"), ("_struct", typ "index \ logic", NoSyn),