--- 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 ***
--- 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}
--- 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"),
--- 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;
--- 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");
--- 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}"