Email Gateway (Aug 18 2022 at 13:18): Email Gateway (Aug 18 2022 at 13:18):From: Tobias Nipkow <nipkow@in.tum.de>
Christian Doczkal wrote:
Replace the "term" command by an antiquotation, eg
text{* @{term "if a then b else c"} *}
That should do the job.
Tobias
Email Gateway (Aug 18 2022 at 13:18):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello
OK, that does indeed work. I expected this to apply not only to
antiquotations but also to the theory itself. Using it this way
introduces notational inconsistencies as the terms have different fonts
in lemmas/proofs than they have in the text body. Is there a way to
extend the scope of these output transformations to the whole theory?
smime.p7s
Email Gateway (Aug 18 2022 at 13:19):From: Tobias Nipkow <nipkow@in.tum.de>
Christian Doczkal wrote:
I'm afraid that is not possible.
Tobias
Email Gateway (Aug 18 2022 at 13:19):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello
Replace the "term" command by an antiquotation, eg
text{* @{term "if a then b else c"} *}
[...]
I'm afraid that is not possible.
What is the fundamental difference between rendering a term in the
theory as latex output and rendering a term in an antiquotation as latex
output? I was expecting that both use the same mechanisms.
smime.p7s
Email Gateway (Aug 18 2022 at 13:20):From: Tobias Nipkow <nipkow@in.tum.de>
Christian Doczkal wrote:
They don't use the same mechanism.
Tobias
Email Gateway (Aug 18 2022 at 13:20):From: Makarius <makarius@sketis.net>
Isabelle document preparation works primarily by presenting the original
sources in a relatively smart way, such that you might think the system
really understands formal notation etc, which it does not.
So if you present
prop "A ==> B"
you will get a slightly ugly ASCII version, corresponding to what is
written in the source. You need to present a "meta-source" to get full
notation, e.g. like this:
text {*
@{prop "A ==> B}
*}
This works, because document antiquotations can present fully internalized
terms by pretty printing them again, according to current print mode
setup. LaTeX sugar heavily depends on this a lot.
Makarius
Email Gateway (Aug 18 2022 at 13:26):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello
I have some minimalistic session containing the theory (importing Main
was well had no effect)
theory SugarTest
imports LaTeXsugar
begin
term "if a then b else c"
end
According to the documentation (sugar.pdf) this should suffice to have
the "if" "then" "else" typeset in sans serif fonts. Unfortunately
neither this not any other syntactic sugar works with my Isabelle
environment. (Isabelle2008)
I uses the standard makefile generated by isatool mkdir and have only
added SugarTest to ROOT.ML Can someone reproduce this? (Whole session is
attached)
Am I missing something or is this really not working?
sugar.tgz
smime.p7s
Last updated: May 03 2024 at 04:19 UTC