--- a/NEWS Tue Dec 10 14:42:56 2024 +0100
+++ b/NEWS Tue Dec 10 16:37:09 2024 +0100
@@ -174,6 +174,29 @@
Isabelle/VSCode extension settings.
+*** Document preparation ***
+
+* LaTeX output from printed entities (types, terms, thms) now contains
+additional markup as follows:
+
+ tclass -- type class "a"
+ tconst -- type constructor "a"
+ tfree -- free type variable "'a"
+ tvar -- schematic type variable "?'a"
+ const -- constant "a"
+ free -- free variable "a"
+ bound -- bound variable "a"
+ skolem -- skolem variable "a"
+ var -- schematic variable "?a"
+
+These markup names are turned into LaTeX macros using the prefix "\isa",
+e.g. "\isaconst{...}" for "const". By default, these macros have no
+effect, but may be defined in root.tex like this:
+
+ \renewcommand{\isatconst}[1]{{\color{darkgray}#1}}
+ \renewcommand{\isaconst}[1]{\textsl{\color{darkgray}#1}}
+
+
*** HOL ***
* Sledgehammer:
--- a/lib/texinputs/isabelle.sty Tue Dec 10 14:42:56 2024 +0100
+++ b/lib/texinputs/isabelle.sty Tue Dec 10 16:37:09 2024 +0100
@@ -151,6 +151,15 @@
{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
\newcommand{\isacommand}[1]{\isakeyword{#1}}
+\newcommand{\isatclass}[1]{#1}
+\newcommand{\isatconst}[1]{#1}
+\newcommand{\isatfree}[1]{#1}
+\newcommand{\isatvar}[1]{#1}
+\newcommand{\isaconst}[1]{#1}
+\newcommand{\isafree}[1]{#1}
+\newcommand{\isaskolem}[1]{#1}
+\newcommand{\isabound}[1]{#1}
+\newcommand{\isavar}[1]{#1}
\newcommand{\isakeywordcontrol}[1]
{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
--- a/src/Pure/General/latex.ML Tue Dec 10 14:42:56 2024 +0100
+++ b/src/Pure/General/latex.ML Tue Dec 10 16:37:09 2024 +0100
@@ -250,8 +250,16 @@
[(Markup.commandN, markup_macro "isacommand"),
(Markup.keyword1N, markup_macro "isacommand"),
(Markup.keyword2N, markup_macro "isakeyword"),
- (Markup.keyword3N, markup_macro"isacommand")
- ];
+ (Markup.keyword3N, markup_macro"isacommand"),
+ (Markup.tclassN, markup_macro"isatclass"),
+ (Markup.tconstN, markup_macro"isatconst"),
+ (Markup.tfreeN, markup_macro"isatfree"),
+ (Markup.tvarN, markup_macro"isatvar"),
+ (Markup.constN, markup_macro"isaconst"),
+ (Markup.freeN, markup_macro"isafree"),
+ (Markup.skolemN, markup_macro"isaskolem"),
+ (Markup.boundN, markup_macro"isabound"),
+ (Markup.varN, markup_macro"isavar")];
fun latex_markup (a, props) =
(if Markup.has_syntax props then NONE else Symtab.lookup markup_latex a)