# 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 \<Rightarrow> float_position", Mixfix.mixfix "_"),
     ("_constify",   typ "num_position \<Rightarrow> num_const",   Mixfix.mixfix "_"),
     ("_constify",   typ "float_position \<Rightarrow> float_const", Mixfix.mixfix "_"),
-    ("_index",      typ "logic \<Rightarrow> index",
-      Mixfix.mixfix "(\<open>unbreakable notation=\<open>mixfix index\<close>\<close>\<^bsub>_\<^esub>)"),
+    ("_index",      typ "logic \<Rightarrow> index", Mixfix.mixfix "(\<open>unbreakable notation=\<open>index\<close>\<close>\<^bsub>_\<^esub>)"),
     ("_indexdefault", typ "index",                     Mixfix.mixfix ""),
     ("_indexvar",   typ "index",                       Mixfix.mixfix "'\<index>"),
     ("_struct",     typ "index \<Rightarrow> logic",              NoSyn),