# HG changeset patch
# User wenzelm
# Date 1728159864 -7200
# Node ID 9e2eb05cc2b7d5784bbe284e6ff6c5a03c0d38bb
# Parent  0c898f7d9b150b86c3abc5cb704ef8078e7e5d44
more inner-syntax markup;

diff -r 0c898f7d9b15 -r 9e2eb05cc2b7 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Oct 05 15:18:49 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Oct 05 22:24:24 2024 +0200
@@ -432,6 +432,9 @@
       its body argument (automatically inserted for @{keyword "binder"}
       annotations, see \secref{sec:binders}).
 
+      \<^item> @{notation_kind_def literal}: notation for literal values, such as
+      string or number.
+
       \<^item> @{notation_kind_def type_application}: application of a type
       constructor to its arguments.
 
diff -r 0c898f7d9b15 -r 9e2eb05cc2b7 src/HOL/String.thy
--- a/src/HOL/String.thy	Sat Oct 05 15:18:49 2024 +0200
+++ b/src/HOL/String.thy	Sat Oct 05 22:24:24 2024 +0200
@@ -224,7 +224,7 @@
 type_synonym string = "char list"
 
 syntax
-  "_String" :: "str_position \<Rightarrow> string"    (\<open>_\<close>)
+  "_String" :: "str_position \<Rightarrow> string"    (\<open>(\<open>notation=\<open>literal string\<close>\<close>_)\<close>)
 
 ML_file \<open>Tools/string_syntax.ML\<close>
 
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>));