Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned markup;
authorwenzelm
Tue, 10 Dec 2024 19:47:47 +0100
changeset 81571 a180b070d4f8
parent 81570 af49ce611685
child 81572 693a95492008
child 81676 1c2a68bb0ff1
tuned markup;
src/Pure/PIDE/markup_kind.ML file | annotate | diff | comparison | revisions
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- 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>));
--- 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),
isabelle