[isabelle] Mixfix syntax in term antiquotation in unnamed context



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.