On 29/12/2020 16:44, Lars Hupel wrote:
>
> we have another problem:
>
> 10:01:16 *** Incoherent use of file name
> "$ISABELLE_HOME/src/Doc/antiquote_setup.ML" as
> "files/ISABELLE_HOME/src/Doc/antiquote_setup.ML.html" in theory
> Isabelle_Meta_Model.Generator_static vs. Isabelle_Meta_Model.Design_deep
I've returned from Christmas vacation yesterday and now see that you have
addressed it already in AFP/459344fb0c40.
The approach looks right: a theory context manages shared resources according
to the import graph structure.
At a later stage, I should probably merge ideas from
"$ISABELLE_HOME/src/Doc/antiquote_setup.ML" back into more official
antiquotations in Isabelle/Pure.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
