Email Gateway (Aug 18 2022 at 14:28): Email Gateway (Aug 18 2022 at 14:28):From: Daniel Wasserrab <daniel.wasserrab@kit.edu>
Hello everyone,
after moving to Isabelle 2009-1, I experience many problems with
document generation. First, I'd like the question marks in printed
theorems to disappear. Until now, I just wrote "reset
show_question_marks" in my ROOT.ML, and all was good. Now, ML won't
accept reset any more. I found something in the NEWS, saying that
show_question_marks is now a flag, and in Pure's term.ML, I found the
following line:
val show_question_marks = Unsynchronized.ref true;
I tried copying this into ROOT.ML and changing true to false, but no
effect. Keeping false, again no effect. So, how can I change this in my
ROOT.ML? Is there still any possibility?
Secondly, until now I used @{thm[mode=Rule] ...} to print nice
derivation rules for my theorems. Also, this does not work any more. The
documentation on the Isabelle website still shows this as the way to go,
and I found nothing in the NEWS describing this problem...
I'm glad to accept any advice :)
..and perhaps the one changing the whole document preperation stuff
writes also an updated LaTeXSugar document...
Regards
Daniel
smime.p7s
Email Gateway (Aug 18 2022 at 14:29):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Daniel,
val show_question_marks = Unsynchronized.ref true;
I tried copying this into ROOT.ML and changing true to false, but no
effect. Keeping false, again no effect. So, how can I change this in my
ROOT.ML? Is there still any possibility?
The line you must insert into your ROOT.ML is
Unsynchronized.reset show_question_marks;
If you would copy the line from term.ML, you would just allocate a new
reference of which the system won't take any notice.
Secondly, until now I used @{thm[mode=Rule] ...} to print nice
derivation rules for my theorems. Also, this does not work any more.
This is indeed strange, but when I rebuild the sugar document the
inference rule is printed as expected, so I do not suspect this to be
broken ;-). If the problem persists, perhaps I could have a look at
your sources to figure out the problem.
Hope this helps,
Florian
signature.asc
Last updated: Apr 19 2024 at 04:17 UTC