Email Gateway (Aug 23 2022 at 09:20): Email Gateway (Aug 23 2022 at 09:20):From: Norbert Schirmer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
After a “Theory.join_theory” a file antiquotation reports an error “no such file” for which it is perfectly happy before the join theory.
Note that the markup displayed in Isabelle/Jedit still appears as expected, only decorated with the error twigglies.
This can be demonstrated by HOl-ex.Join_Theory.thy
Join_Theory_Error.png
Join_Theory_Markup.png
Join_Theory.thy
Email Gateway (Aug 23 2022 at 09:21):From: Makarius <makarius@sketis.net>
The problem is that Theory.join_theory performs a regular theory merge, which
historically appeared only in theory header position. Thus a few data slots
are reset to an empty value, notably the master directory of the theory: this
makes the @{file} antiquotation fail.
For now you can use the following change on Isabelle2020:
https://isabelle.sketis.net/repos/isabelle/rev/2c7cfd2f9b6c
But this is not the last word: some more data slots need to be treated
similarly. I will probably also change the Theory_Data API to discontinue the
"extend" operation and its implicit impact on the "merge" operation. In those
rare cases where non-standard extend/merge is required, it can be done via
Theory.at_begin (e.g. see
https://isabelle.sketis.net/repos/isabelle/rev/b9e9ff3a1e1c).
Makarius
Last updated: Apr 23 2024 at 20:15 UTC