Email Gateway (Aug 19 2022 at 10:50): Email Gateway (Aug 19 2022 at 10:50):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
Isabelle2013's behaviour in the following example surprises me:
context fixes r :: nat begin
definition foo :: "nat => nat" ("\<bla> _" 50)
where "\<bla> n = r" -- {* @{term "\<bla> 0"} *}
text {* @{term "\<bla> 0"} *}
end
In jEdit (and the build tool), the antiquotation in -- {* *} complains about an
"inner lexical error at: \<bla> 0". In ProofGeneral, Isabelle accepts this antiquotation
(xemacs 21.4.21, PG 3.7.1.1). The antiquotation inside text {* *} is fine.
Isabelle/jEdit also accepts the antiquotation in -- {* *} when the definition of foo does
not refer to the parameters of the context (for example, replace "\<bla> n = r" with
"\<bla> n = 0").
If I use -- {* @{term "foo 0"} *}, everything works fine, but Isabelle prints "foo 0" also
in the generated document. I really would like to have "\<bla> 0" in the document. How can
I achieve this? (In my use case, foo is a lengthy definition with fun and the -- is some
comment in the middle of the definition, so just using text after the definition does not
work).
And a more general question: Why do jEdit and PG differ here?
Andreas
Last updated: Apr 24 2024 at 16:18 UTC