# HG changeset patch
# User wenzelm
# Date 1735765587 -3600
# Node ID 9253dadbd4aca83c2c6bd0d97d7fa8dc9b9a1147
# Parent  7c3f7e992889546e02a32ad1bbf5a00f7e823b1b
revert changeset 2f98e3c4592c: avoid conflict with low-level \<^latex> markup;

diff -r 7c3f7e992889 -r 9253dadbd4ac NEWS
--- a/NEWS	Wed Jan 01 19:42:53 2025 +0100
+++ b/NEWS	Wed Jan 01 22:06:27 2025 +0100
@@ -209,17 +209,15 @@
   \renewcommand{\isatconst}[1]{{\color{darkgray}#1}}
   \renewcommand{\isaconst}[1]{\textsl{\color{darkgray}#1}}
 
-* LaTeX presentation now distinguishes keywords of outer and inner
-syntax more carefully. This allows to imitate Isabelle/jEdit rendering
-like this:
+* LaTeX presentation of outer syntax keywords now distinguishes
+keyword1, keyword2, keyword3 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 ***
diff -r 7c3f7e992889 -r 9253dadbd4ac lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Wed Jan 01 19:42:53 2025 +0100
+++ b/lib/texinputs/isabelle.sty	Wed Jan 01 22:06:27 2025 +0100
@@ -154,8 +154,6 @@
 \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}
diff -r 7c3f7e992889 -r 9253dadbd4ac src/Pure/General/latex.ML
--- a/src/Pure/General/latex.ML	Wed Jan 01 19:42:53 2025 +0100
+++ b/src/Pure/General/latex.ML	Wed Jan 01 22:06:27 2025 +0100
@@ -251,8 +251,6 @@
    (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"),