# HG changeset patch
# User wenzelm
# Date 1733845029 -3600
# Node ID f8b28356ab94c0e316e5d77181c3ae50f92c1468
# Parent  e88cf59244ee8b77248321cd5257ef24d5600947
more LaTeX markup for printed entities;

diff -r e88cf59244ee -r f8b28356ab94 NEWS
--- 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:
diff -r e88cf59244ee -r f8b28356ab94 lib/texinputs/isabelle.sty
--- 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\,}}
diff -r e88cf59244ee -r f8b28356ab94 src/Pure/General/latex.ML
--- 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)