Dear all,
Unfortunately, Mirabelle is broken since aa8dce9ab8a9 ('discontinued
legacy load path;'). It relied on the implicit path, since it generates
a modified version of a theory file somewhere in /tmp, and then
processes that file using 'use_thy' in a raw isabelle_process. The
imports of
So I am wondering if the system could provide a variant of use_thy(s),
which takes an explicit master path and basically interprets the given
theory as if it would reside in that path. Probably, similar
functionality is already available for PG interaction. Of course any
other solution would
On Fri, 4 Mar 2011, Makarius wrote:
On Fri, 4 Mar 2011, Alexander Krauss wrote:
What I was asking for is a possibility to load a theory file A.thy from
location X (here: the location of the modified theory file in /tmp) with a
master path pointing to location Y (here: the original location
