Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] File antiquotation broken after Theory.join_th...


view this post on Zulip Email Gateway (Jul 15 2020 at 14:34):

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

view this post on Zulip Email Gateway (Jul 16 2020 at 21:07):

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: Dec 05 2021 at 22:18 UTC