Email Gateway (Oct 25 2024 at 20:35): Email Gateway (Oct 25 2024 at 20:35):From: Tobias Nipkow <nipkow@in.tum.de>
How can I tell Isabelle what size some \<^latex> notation is?
Exmaple: If I want to print "map" a certain way, eg in a certain font
notation (latex) map ("\<^latex>‹...›")
Isabelle seems to assume that "..." takes less space than "map".
How much space does Isabelle reserve for a piece of \<^latex>?
Is there any way to tell Isabelle how much space it should reserve?
Thanks
Tobias
Email Gateway (Oct 26 2024 at 06:08):From: Tobias Nipkow <nipkow@in.tum.de>
I think I have figured it out by now: you have to separate the latex control
parts (and put them into \<^latex>, which is probably assumed to take 0 space)
from the actual text. In my case:
notation (latex) map ("\<^latex>‹...›map\<^latex>‹...›")
Tobias
On 25/10/2024 22:35, Tobias Nipkow wrote:
How can I tell Isabelle what size some \<^latex> notation is?
Exmaple: If I want to print "map" a certain way, eg in a certain font
notation (latex) map ("\<^latex>‹...›")
Isabelle seems to assume that "..." takes less space than "map".
How much space does Isabelle reserve for a piece of \<^latex>?
Is there any way to tell Isabelle how much space it should reserve?Thanks
Tobias
Email Gateway (Oct 26 2024 at 12:22):From: Makarius <makarius@sketis.net>
On 25/10/2024 22:35, Tobias Nipkow wrote:
How can I tell Isabelle what size some \<^latex> notation is?
Exmaple: If I want to print "map" a certain way, eg in a certain font
notation (latex) map ("\<^latex>‹...›")
Isabelle seems to assume that "..." takes less space than "map".
How much space does Isabelle reserve for a piece of \<^latex>?
Is there any way to tell Isabelle how much space it should reserve?
On 26/10/2024 08:07, Tobias Nipkow wrote:
I think I have figured it out by now: you have to separate the latex control
parts (and put them into \<^latex>, which is probably assumed to take 0 space)
from the actual text. In my case:notation (latex) map ("\<^latex>‹...›map\<^latex>‹...›")
Control symbols indeed have length 0 in pretty-printed output; the \<^latex>
symbol with its cartouche argument is treated like a single control symbol.
In your second attempt, I guess that the Latex snippets contain macros to
suppress the plain text?
Here is a more explicit example for type "fun":
type_notation (latex) "fun" (‹(_/
\<^latex>‹{\isasymlongrightarrow}\ignore{›aa\<^latex>‹}› _)› [1, 0] 0)
The plain text "aa" is only there to measure the size. The Latex macro \ignore
will drop it from the printed output:
\newcommand{\ignore}[1]{}
There might be better tricks --- I am not the LaTeX-sugar wizard.
Or rather it might be time to think about syntax for options in
\<^control>CARTOUCHE notation. It could be used here elsewhere, e.g. in
regular antiquotations. For example:
\<^latex>‹\<^options>‹width=2›{\isasymlongrightarrow}›
\<^typ>‹\<^options>‹margin=40, display› 'a ⇒ 'a›
Thus we could discontinue the old antiquotation syntax @{typ [margin=40,
display] "'a ⇒ 'a"} eventually.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC