Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: more LaTeX markup

Email Gateway (Dec 11 2024 at 00:53):

From: Makarius <makarius@sketis.net>
* 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}}

This refers to Isabelle/f8b28356ab94.

It has required many decades to get to that point: I now recallthat in the
late 1990ies, we could only get free/bound/var etc. but not the consts. Thanks
to major cleanup of the inner-syntax framework some months ago, this now
turned out reasonably easy.

Makarius

Email Gateway (Dec 11 2024 at 16:25):

From: Tobias Nipkow <nipkow@in.tum.de>
Brilliant, many thanks!

Is there any way to obtain (in the document} \isaconst{Nil} via some antiquotation?

• @{const Nil} produces []
• @{const [source] Nil} produces \isa{Nil}

Of course this is just an example standing for the many constants that have
associated syntax.

Tobias

On 10/12/2024 22:13, Makarius wrote:

* 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}}

This refers to Isabelle/f8b28356ab94.

It has required many decades to get to that point: I now recallthat in the late
1990ies, we could only get free/bound/var etc. but not the consts. Thanks to
major cleanup of the inner-syntax framework some months ago, this now turned out
reasonably easy.

Makarius

smime.p7s

Email Gateway (Dec 13 2024 at 14:04):

From: Makarius <makarius@sketis.net>
On 11/12/2024 17:25, Tobias Nipkow wrote:

Is there any way to obtain (in the document} \isaconst{Nil} via some
antiquotation?
- @{const Nil} produces []
- @{const [source] Nil} produces \isa{Nil}

Of course this is just an example standing for the many constants that have
associated syntax.

@{const [source] NAME} presents the original input source, not pretty-printed
output. It would require substantial reworking of the document preparation
system to use PIDE markup there: one happy day that will happen, but not now
and not for the coming release.

If this is actually about printing formal entity names like the term
pretty-printer does (without syntax), you can define a document antiquotation
@{const_name NAME} like this:

setup ‹
Document_Output.antiquotation_pretty_embedded \<^binding>‹const_name›
(Args.const {proper = true, strict = false})
(fn ctxt => fn c => Pretty.mark_str (Markup.const,
Proof_Context.extern_const ctxt c))
›

Makarius

Email Gateway (Dec 16 2024 at 12:59):

From: Tobias Nipkow <nipkow@in.tum.de>
That was exactly what I needed, many thanks!

Tobias

On 13/12/2024 13:46, Makarius wrote:

On 11/12/2024 17:25, Tobias Nipkow wrote:

Is there any way to obtain (in the document} \isaconst{Nil} via some
antiquotation?
- @{const Nil} produces []
- @{const [source] Nil} produces \isa{Nil}

Of course this is just an example standing for the many constants that have
associated syntax.

@{const [source] NAME} presents the original input source, not pretty-printed
output. It would require substantial reworking of the document preparation
system to use PIDE markup there: one happy day that will happen, but not now and
not for the coming release.

If this is actually about printing formal entity names like the term pretty-
printer does (without syntax), you can define a document antiquotation
@{const_name NAME} like this:

setup ‹
  Document_Output.antiquotation_pretty_embedded \<^binding>‹const_name›
    (Args.const {proper = true, strict = false})
    (fn ctxt => fn c => Pretty.mark_str (Markup.const,
Proof_Context.extern_const ctxt c))
›

Makarius

smime.p7s

Email Gateway (Dec 23 2024 at 08:31):

From: Tobias Nipkow <nipkow@in.tum.de>
Hi Makarius,

I am using these new macros to modify the font for constants. This works very
well except for one issue: in latex blocks with line breaks, the \isaindent code
does not utilize these macros but includes the bare names only. As a result, the
indentation is a bit off. Here is an example of the generated latex code

\isaindent{{\isacharequal}{\kern0pt}\
{\isacharparenleft}{\kern0pt}}\isaconst{LT}\ {\isasymRightarrow}\
\isakeyword{let}\ \isabound{l{\isacharprime}{\kern0pt}}\
{\isacharequal}{\kern0pt}\ \isaconst{del}\ \isavar{x}\ \isavar{l}\isanewline
\isaindent{{\isacharequal}{\kern0pt}\ {\isacharparenleft}{\kern0pt}LT\
{\isasymRightarrow}\ }

\isaconst{LT} vs plain LT inside an \isaindent a few lines below.

Tobias

On 10/12/2024 22:13, Makarius wrote:

* 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}}

This refers to Isabelle/f8b28356ab94.

It has required many decades to get to that point: I now recallthat in the late
1990ies, we could only get free/bound/var etc. but not the consts. Thanks to
major cleanup of the inner-syntax framework some months ago, this now turned out
reasonably easy.

Makarius

smime.p7s

Email Gateway (Jan 03 2025 at 19:03):

From: Makarius <makarius@sketis.net>
On 23/12/2024 09:31, Tobias Nipkow wrote:

I am using these new macros to modify the font for constants. This works very
well except for one issue: in latex blocks with line breaks, the \isaindent
code does not utilize these macros but includes the bare names only.

This should work better in recent Isabelle/9253dadbd4ac: I had to make
significant changes to pretty-printing with markup for that. A few more
changes might be coming a bit later ...

Makarius

Email Gateway (Jan 05 2025 at 06:45):

From: Tobias Nipkow <nipkow@in.tum.de>
Thanks Makarius, it works perfectly.

Tobias

On 03/01/2025 20:03, Makarius wrote:

On 23/12/2024 09:31, Tobias Nipkow wrote:

I am using these new macros to modify the font for constants. This works very
well except for one issue: in latex blocks with line breaks, the \isaindent
code does not utilize these macros but includes the bare names only.

This should work better in recent Isabelle/9253dadbd4ac: I had to make
significant changes to pretty-printing with markup for that. A few more changes
might be coming a bit later ...

Makarius

smime.p7s

Email Gateway (Jan 07 2025 at 07:40):

From: Tobias Nipkow <nipkow@in.tum.de>
Makarius,

Just one more thing: the field names in record updates are not enclosed in any
macro, eg the field "front":

\isa{\isafree{q}{\isasymlparr}front\
{\isacharcolon}{\kern0pt}{\isacharequal}{\kern0pt}\
{\isacharbrackleft}{\kern0pt}{\isacharbrackright}{\kern0pt}{\isasymrparr}}.

Can you wrap them in \isaconst (because the field selector is a function)?

Thanks
Tobias

On 03/01/2025 20:03, Makarius wrote:

On 23/12/2024 09:31, Tobias Nipkow wrote:

I am using these new macros to modify the font for constants. This works very
well except for one issue: in latex blocks with line breaks, the \isaindent
code does not utilize these macros but includes the bare names only.

This should work better in recent Isabelle/9253dadbd4ac: I had to make
significant changes to pretty-printing with markup for that. A few more changes
might be coming a bit later ...

Makarius

smime.p7s

Email Gateway (Jan 07 2025 at 22:04):

From: Makarius <makarius@sketis.net>
On 07/01/2025 08:40, Tobias Nipkow wrote:

Just one more thing: the field names in record updates are not enclosed in any
macro, eg the field "front":

Can you wrap them in \isaconst (because the field selector is a function)?

This turned out quite easy, using mixfix markup for the specific record
syntax: https://isabelle-dev.sketis.net/rISABELLE4b739ed65946

I have also had a look at theory src/HOL/Library/Datatype_Records.thy but its
output syntax appears to be somewhat unfinished anyway.

Makarius

Email Gateway (Jan 08 2025 at 10:06):

From: Tobias Nipkow <nipkow@in.tum.de>
Sweet, thanks!

Tobias

On 07/01/2025 23:04, Makarius wrote:

On 07/01/2025 08:40, Tobias Nipkow wrote:

Just one more thing: the field names in record updates are not enclosed in any
macro, eg the field "front":

Can you wrap them in \isaconst (because the field selector is a function)?

This turned out quite easy, using mixfix markup for the specific record syntax:
https://isabelle-dev.sketis.net/rISABELLE4b739ed65946

I have also had a look at theory src/HOL/Library/Datatype_Records.thy but its
output syntax appears to be somewhat unfinished anyway.

Makarius

smime.p7s

Last updated: Feb 01 2025 at 20:19 UTC