[isabelle-dev] Incoherent use of file name "hoare_syntax.ML"

[Makarius]

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