# HG changeset patch
# User wenzelm
# Date 1734526195 -3600
# Node ID e5be995d21f0846a084a99b24de1bdf11b112621
# Parent  079dee3b117cc4cca68cdd375c50712564dcb3d7
clarified LaTeX presentation: more specific keywords;

diff -r 079dee3b117c -r e5be995d21f0 NEWS
--- a/NEWS	Wed Dec 18 12:49:42 2024 +0100
+++ b/NEWS	Wed Dec 18 13:49:55 2024 +0100
@@ -209,6 +209,16 @@
   \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:
+
+  \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}}
+
+
 
 *** HOL ***
 
diff -r 079dee3b117c -r e5be995d21f0 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Wed Dec 18 12:49:42 2024 +0100
+++ b/lib/texinputs/isabelle.sty	Wed Dec 18 13:49:55 2024 +0100
@@ -151,6 +151,9 @@
 {\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
 \newcommand{\isacommand}[1]{\isakeyword{#1}}
+\newcommand{\isakeywordONE}[1]{\isakeyword{#1}}
+\newcommand{\isakeywordTWO}[1]{\isakeyword{#1}}
+\newcommand{\isakeywordTHREE}[1]{\isakeyword{#1}}
 \newcommand{\isatclass}[1]{#1}
 \newcommand{\isatconst}[1]{#1}
 \newcommand{\isatfree}[1]{#1}
diff -r 079dee3b117c -r e5be995d21f0 src/Pure/General/latex.ML
--- a/src/Pure/General/latex.ML	Wed Dec 18 12:49:42 2024 +0100
+++ b/src/Pure/General/latex.ML	Wed Dec 18 13:49:55 2024 +0100
@@ -247,10 +247,10 @@
 val markup_indent = markup_macro "isaindent";
 val markup_latex =
  Symtab.make
-  [(Markup.commandN, markup_macro "isacommand"),
-   (Markup.keyword1N, markup_macro "isacommand"),
-   (Markup.keyword2N, markup_macro "isakeyword"),
-   (Markup.keyword3N, markup_macro "isacommand"),
+  [(Markup.commandN, markup_macro "isakeywordONE"),
+   (Markup.keyword1N, markup_macro "isakeywordONE"),
+   (Markup.keyword2N, markup_macro "isakeywordTWO"),
+   (Markup.keyword3N, markup_macro "isakeywordTHREE"),
    (Markup.tclassN, markup_macro "isatclass"),
    (Markup.tconstN, markup_macro "isatconst"),
    (Markup.tfreeN, markup_macro "isatfree"),
diff -r 079dee3b117c -r e5be995d21f0 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed Dec 18 12:49:42 2024 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Dec 18 13:49:55 2024 +0100
@@ -80,6 +80,7 @@
   val is_proof_open: keywords -> string -> bool
   val is_proof_close: keywords -> string -> bool
   val is_proof_asm: keywords -> string -> bool
+  val is_proof_asm_goal: keywords -> string -> bool
   val is_improper: keywords -> string -> bool
   val is_printed: keywords -> string -> bool
 end;
@@ -289,6 +290,7 @@
 val is_proof_close = command_category [qed, qed_script, qed_block, prf_close];
 
 val is_proof_asm = command_category [prf_asm, prf_asm_goal];
+val is_proof_asm_goal = command_category [prf_asm_goal];
 val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
 
 fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
diff -r 079dee3b117c -r e5be995d21f0 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Wed Dec 18 12:49:42 2024 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Wed Dec 18 13:49:55 2024 +0100
@@ -437,7 +437,7 @@
 
 val _ =
   Theory.setup
-   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "isacommand" #>
+   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "isakeywordONE" #>
     entity_antiquotation \<^binding>\<open>method\<close> Method.check_name "isa" #>
     entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name "isa");
 
diff -r 079dee3b117c -r e5be995d21f0 src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Wed Dec 18 12:49:42 2024 +0100
+++ b/src/Pure/Thy/document_output.ML	Wed Dec 18 13:49:55 2024 +0100
@@ -159,16 +159,27 @@
 
 fun output_token ctxt tok =
   let
+    val keywords = Thy_Header.get_keywords' ctxt;
+
     fun output antiq bg en =
       output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
   in
     (case Token.kind_of tok of
       Token.Comment NONE => []
     | Token.Comment (SOME Comment.Marker) => []
-    | Token.Command => output false "\\isacommand{" "}"
+    | Token.Command =>
+        let
+          val name = (Token.content_of tok);
+          val bg =
+            if Keyword.is_theory_end keywords name then "\\isakeywordTWO{"
+            else if Keyword.is_proof_asm keywords name orelse
+              Keyword.is_proof_asm_goal keywords name then "\\isakeywordTHREE{"
+            else if Keyword.is_proof_asm_goal keywords name then "\\isakeywordTHREE{"
+            else "\\isakeywordONE{";
+        in output false bg "}" end
     | Token.Keyword =>
         if Symbol.is_ascii_identifier (Token.content_of tok)
-        then output false "\\isakeyword{" "}"
+        then output false "\\isakeywordTWO{" "}"
         else output false "" ""
     | Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}"
     | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"