more inner-syntax markup, without pretty blocks;

--- a/src/HOL/Library/Numeral_Type.thy	Sun Oct 06 21:55:31 2024 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Sun Oct 06 22:56:07 2024 +0200
@@ -523,13 +523,9 @@
 subsection \<open>Syntax\<close>
 
 syntax
-  "_NumeralType" :: "num_token => type"  (\<open>_\<close>)
-  "_NumeralType0" :: type (\<open>0\<close>)
-  "_NumeralType1" :: type (\<open>1\<close>)
-
-syntax_types
-  "_NumeralType0" == num0 and
-  "_NumeralType1" == num1
+  "_NumeralType" :: "num_token => type"  (\<open>(\<open>open_block notation=\<open>type_literal number\<close>\<close>_)\<close>)
+  "_NumeralType0" :: type (\<open>(\<open>open_block notation=\<open>type_literal number\<close>\<close>0)\<close>)
+  "_NumeralType1" :: type (\<open>(\<open>open_block notation=\<open>type_literal number\<close>\<close>1)\<close>)
 
 translations
   (type) "1" == (type) "num1"

--- a/src/HOL/Num.thy	Sun Oct 06 21:55:31 2024 +0200
+++ b/src/HOL/Num.thy	Sun Oct 06 22:56:07 2024 +0200
@@ -302,7 +302,7 @@
 text \<open>Numeral syntax.\<close>
 
 syntax
-  "_Numeral" :: "num_const \<Rightarrow> 'a"    (\<open>_\<close>)
+  "_Numeral" :: "num_const \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>literal number\<close>\<close>_)\<close>)
 
 ML_file \<open>Tools/numeral.ML\<close>
 

--- a/src/HOL/Rat.thy	Sun Oct 06 21:55:31 2024 +0200
+++ b/src/HOL/Rat.thy	Sun Oct 06 22:56:07 2024 +0200
@@ -1155,7 +1155,7 @@
 
 subsection \<open>Float syntax\<close>
 
-syntax "_Float" :: "float_const \<Rightarrow> 'a"    (\<open>_\<close>)
+syntax "_Float" :: "float_const \<Rightarrow> 'a"    (\<open>(\<open>open_block notation=\<open>literal number\<close>\<close>_)\<close>)
 
 parse_translation \<open>
   let

--- a/src/HOL/String.thy	Sun Oct 06 21:55:31 2024 +0200
+++ b/src/HOL/String.thy	Sun Oct 06 22:56:07 2024 +0200
@@ -216,15 +216,15 @@
   by (cases c) simp
 
 syntax
-  "_Char" :: "str_position \<Rightarrow> char"    (\<open>CHR _\<close>)
-  "_Char_ord" :: "num_const \<Rightarrow> char"   (\<open>CHR _\<close>)
+  "_Char" :: "str_position \<Rightarrow> char"    (\<open>(\<open>open_block notation=\<open>literal char\<close>\<close>CHR _)\<close>)
+  "_Char_ord" :: "num_const \<Rightarrow> char"   (\<open>(\<open>open_block notation=\<open>literal char code\<close>\<close>CHR _)\<close>)
 syntax_consts
   "_Char" "_Char_ord" \<rightleftharpoons> Char
 
 type_synonym string = "char list"
 
 syntax
-  "_String" :: "str_position \<Rightarrow> string"    (\<open>(\<open>notation=\<open>literal string\<close>\<close>_)\<close>)
+  "_String" :: "str_position \<Rightarrow> string"    (\<open>(\<open>open_block notation=\<open>literal string\<close>\<close>_)\<close>)
 
 ML_file \<open>Tools/string_syntax.ML\<close>
 
@@ -522,8 +522,10 @@
 code_datatype "0 :: String.literal" String.Literal
 
 syntax
-  "_Literal" :: "str_position \<Rightarrow> String.literal"   (\<open>STR _\<close>)
-  "_Ascii" :: "num_const \<Rightarrow> String.literal"        (\<open>STR _\<close>)
+  "_Literal" :: "str_position \<Rightarrow> String.literal"
+    (\<open>(\<open>open_block notation=\<open>literal string\<close>\<close>STR _)\<close>)
+  "_Ascii" :: "num_const \<Rightarrow> String.literal"
+    (\<open>(\<open>open_block notation=\<open>literal char code\<close>\<close>STR _)\<close>)
 syntax_consts
   "_Literal" "_Ascii" \<rightleftharpoons> String.Literal
 

--- a/src/Pure/PIDE/markup_kind.ML	Sun Oct 06 21:55:31 2024 +0200
+++ b/src/Pure/PIDE/markup_kind.ML	Sun Oct 06 22:56:07 2024 +0200
@@ -22,6 +22,7 @@
   val markup_postfix: Markup.T
   val markup_infix: Markup.T
   val markup_binder: Markup.T
+  val markup_type_literal: Markup.T
   val markup_literal: Markup.T
   val markup_type_application: Markup.T
   val markup_application: Markup.T
@@ -101,6 +102,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_type_literal = setup_notation (Binding.make ("type_literal", \<^here>));
 val markup_literal = setup_notation (Binding.make ("literal", \<^here>));
 
 val markup_type_application = setup_notation (Binding.make ("type_application", \<^here>));

--- a/src/Pure/pure_thy.ML	Sun Oct 06 21:55:31 2024 +0200
+++ b/src/Pure/pure_thy.ML	Sun Oct 06 22:56:07 2024 +0200
@@ -113,11 +113,14 @@
     ("_class_name", typ "id \<Rightarrow> class_name",            Mixfix.mixfix "_"),
     ("_class_name", typ "longid \<Rightarrow> class_name",        Mixfix.mixfix "_"),
     ("_dummy_sort", typ "sort",                        Mixfix.mixfix "'_"),
-    ("_topsort",    typ "sort",                        Mixfix.mixfix "{}"),
-    ("_sort",       typ "classes \<Rightarrow> sort",             Mixfix.mixfix "{_}"),
+    ("_topsort",    typ "sort",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>mixfix sort\<close>\<close>{})"),
+    ("_sort",       typ "classes \<Rightarrow> sort",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>mixfix sort\<close>\<close>{_})"),
     ("",            typ "class_name \<Rightarrow> classes",       Mixfix.mixfix "_"),
     ("_classes",    typ "class_name \<Rightarrow> classes \<Rightarrow> classes", Mixfix.mixfix "_,_"),
-    ("_tapp",       typ "type \<Rightarrow> type_name \<Rightarrow> type",   mixfix ("_ _", [1000, 0], 1000)),
+    ("_tapp",       typ "type \<Rightarrow> type_name \<Rightarrow> type",
+      mixfix ("(\<open>open_block notation=\<open>type_application\<close>\<close>_ _)", [1000, 0], 1000)),
     ("_tappl",      typ "type \<Rightarrow> types \<Rightarrow> type_name \<Rightarrow> type",
       Mixfix.mixfix "(\<open>notation=type_application\<close>(1'(_,/ _')) _)"),
     ("",            typ "type \<Rightarrow> types",               Mixfix.mixfix "_"),
@@ -149,7 +152,8 @@
     ("",            typ "longid_position \<Rightarrow> aprop",    Mixfix.mixfix "_"),
     ("",            typ "var_position \<Rightarrow> aprop",       Mixfix.mixfix "_"),
     ("_DDDOT",      typ "aprop",                       Mixfix.mixfix "\<dots>"),
-    ("_aprop",      typ "aprop \<Rightarrow> prop",               Mixfix.mixfix "PROP _"),
+    ("_aprop",      typ "aprop \<Rightarrow> prop",
+      Mixfix.mixfix "(\<open>open_block notation=\<open>mixfix atomic prop\<close>\<close>PROP _)"),
     ("_asm",        typ "prop \<Rightarrow> asms",                Mixfix.mixfix "_"),
     ("_asms",       typ "prop \<Rightarrow> asms \<Rightarrow> asms",        Mixfix.mixfix "_;/ _"),
     ("_bigimpl",    typ "asms \<Rightarrow> prop \<Rightarrow> prop",

--- a/src/ZF/Bin.thy	Sun Oct 06 21:55:31 2024 +0200
+++ b/src/ZF/Bin.thy	Sun Oct 06 22:56:07 2024 +0200
@@ -114,8 +114,8 @@
   "#-2" \<rightleftharpoons> "CONST integ_of(CONST Min BIT 0)"
 
 syntax
-  "_Int" :: "num_token \<Rightarrow> i"  (\<open>#_\<close> 1000)
-  "_Neg_Int" :: "num_token \<Rightarrow> i"  (\<open>#-_\<close> 1000)
+  "_Int" :: "num_token \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>literal number\<close>\<close>#_)\<close> 1000)
+  "_Neg_Int" :: "num_token \<Rightarrow> i"  (\<open>(\<open>open_block notation=\<open>literal number\<close>\<close>#-_)\<close> 1000)
 
 syntax_consts
   "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of