--- a/NEWS Fri Dec 27 19:57:55 2024 +0100
+++ b/NEWS Sat Dec 28 15:43:30 2024 +0100
@@ -209,15 +209,17 @@
\renewcommand{\isatconst}[1]{{\color{darkgray}#1}}
\renewcommand{\isaconst}[1]{\textsl{\color{darkgray}#1}}
-* LaTeX presentation of outer syntax keywords now distinguishes
-keyword1, keyword2, keyword3 more carefully. This allows to imitate
-Isabelle/jEdit rendering like this:
+* LaTeX presentation now distinguishes keywords of outer and inner
+syntax more carefully. This allows to imitate Isabelle/jEdit rendering
+like this:
\renewcommand{\isacommand}[1]{\isakeywordONE{#1}}
\renewcommand{\isakeywordONE}[1]{\isakeyword{\color[RGB]{0,102,153}#1}}
\renewcommand{\isakeywordTWO}[1]{\isakeyword{\color[RGB]{0,153,102}#1}}
\renewcommand{\isakeywordTHREE}[1]{\isakeyword{\color[RGB]{0,153,255}#1}}
+ \renewcommand{\isaliteral}[1]{\isakeyword{\color[RGB]{0,102,153}#1}}
+ \renewcommand{\isadelimiter}[1]{#1}
*** HOL ***
--- a/lib/texinputs/isabelle.sty Fri Dec 27 19:57:55 2024 +0100
+++ b/lib/texinputs/isabelle.sty Sat Dec 28 15:43:30 2024 +0100
@@ -154,6 +154,8 @@
\newcommand{\isakeywordONE}[1]{\isakeyword{#1}}
\newcommand{\isakeywordTWO}[1]{\isakeyword{#1}}
\newcommand{\isakeywordTHREE}[1]{\isakeyword{#1}}
+\newcommand{\isaliteral}[1]{#1}
+\newcommand{\isadelimiter}[1]{#1}
\newcommand{\isatclass}[1]{#1}
\newcommand{\isatconst}[1]{#1}
\newcommand{\isatfree}[1]{#1}
--- a/src/Pure/General/latex.ML Fri Dec 27 19:57:55 2024 +0100
+++ b/src/Pure/General/latex.ML Sat Dec 28 15:43:30 2024 +0100
@@ -251,6 +251,8 @@
(Markup.keyword1N, markup_macro "isakeywordONE"),
(Markup.keyword2N, markup_macro "isakeywordTWO"),
(Markup.keyword3N, markup_macro "isakeywordTHREE"),
+ (Markup.literalN, markup_macro "isaliteral"),
+ (Markup.delimiterN, markup_macro "isadelimiter"),
(Markup.tclassN, markup_macro "isatclass"),
(Markup.tconstN, markup_macro "isatconst"),
(Markup.tfreeN, markup_macro "isatfree"),