Email Gateway (Aug 18 2022 at 17:37): Email Gateway (Aug 18 2022 at 17:37):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Hello all,
While compiling generated documents from theories, it seems some symbols of
Monad_Syntax are missing. Should they be defined in isabellesym.sty ?
Monad_Syntax.tex:37: Undefined control sequence \frqq.
Monad_Syntax.tex:41: Undefined control sequence \isasymbind.
Monad_Syntax.tex:81: Undefined control sequence \isasymthen.
Thanks,
Mathieu
Email Gateway (Aug 18 2022 at 17:37):From: Alexander Krauss <krauss@in.tum.de>
Hi Matthieu,
While compiling generated documents from theories, it seems some symbols of
Monad_Syntax are missing. Should they be defined in isabellesym.sty ?
As a user, you are free to define your own latex renderings of these
symbols... But we should probably add a sensible default...
Monad_Syntax.tex:37: Undefined control sequence \frqq.
This one requires
\usepackage[english]{babel}
Alex
Email Gateway (Aug 18 2022 at 17:37):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Ok, I had just thought it was an omission.
By the way, I discovered the "do_notation" mode allowing to display monadic
terms with the do-notation in antiquotations as well as in "term", "thm" (and
perhaps others?):
thm (do_notation) Ref.change_def
text {* @{thm [mode=do_notation] Ref.change_def} *}
Could this mode be set in a global way to be used by default in
antiquotations? and also in proofs?
Mathieu
Email Gateway (Aug 18 2022 at 17:37):From: Makarius <makarius@sketis.net>
On Tue, 26 Apr 2011, Mathieu Giorgino wrote:
Le mardi 26 avril 2011 09:38:49, Alexander Krauss a écrit :
Hi Matthieu,
While compiling generated documents from theories, it seems some symbols
of Monad_Syntax are missing. Should they be defined in isabellesym.sty ?As a user, you are free to define your own latex renderings of these
symbols... But we should probably add a sensible default...Ok, I had just thought it was an omission.
Isabelle provides infinitely many symbols, but only a finite list of
well-known ones are defined in the default LaTeX styles. This is done in
a way that avoids conflicts of LaTeX packages, i.e. isabellesym.sty does
not force any packages on the user.
thm (do_notation) Ref.change_def
text {* @{thm [mode=do_notation] Ref.change_def} *}
Could this mode be set in a global way to be used by default in
antiquotations? and also in proofs?
This is the normal Isabelle "print mode". You can modify it in some
command line tools like "usedir" using option -m, for example. For
document preparation there is a global default Thy_Output.modes, which can
be set in ROOT.ML.
Makarius
Email Gateway (Aug 18 2022 at 17:38):From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Isabelle provides infinitely many symbols, but only a finite list of
well-known ones are defined in the default LaTeX styles. This is done in
a way that avoids conflicts of LaTeX packages, i.e. isabellesym.sty does
not force any packages on the user.
OK
thm (do_notation) Ref.change_def
text {* @{thm [mode=do_notation] Ref.change_def} *}
Could this mode be set in a global way to be used by default in
antiquotations? and also in proofs?This is the normal Isabelle "print mode". You can modify it in some
command line tools like "usedir" using option -m, for example. For
document preparation there is a global default Thy_Output.modes, which can
be set in ROOT.ML.
OK, I think these are the good way to do it:
for document preparation in ROOT.ML:
Unsynchronized.change Thy_Output.modes (insert (op =) "do_notation");
for display:
ML{* Unsynchronized.change print_mode (insert (op =) "do_notation") *}
To be able to have some exceptions, I have also added an other option to
antiquotations:
fun without_modes modes f x =
let val modes' = subtract (op =) modes (Print_Mode.print_mode_value ())
in Print_Mode.setmp modes' f x end;
val _ = Thy_Output.add_option "rmmode"
(Thy_Output.add_wrapper o without_modes o single);
Thanks,
Mathieu
Email Gateway (Aug 18 2022 at 17:38):From: Makarius <makarius@sketis.net>
I am about to see if \<bind> and \<then> can be included in
isabellesym.sty by default.
Makarius
Last updated: May 06 2024 at 12:29 UTC