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 of the
theory file). Then, the dependencies of A will be found in path Y.
Currently, the only chance of running A.thy successfully (in batch mode) is
to physically place it in the directory where its dependencies are. This is
somewhat rigid and problematic for Mirabelle.
In that case Mirablle can copy all sources to /tmp and then poke around.
The included example theory shows how to embed transactions with generated
position information.
Makariustheory A imports Main
begin
Isabelle.command ("file"="A.thy", "line"="1") "definition \"foo = 0\""
Isabelle.command ("file"="A.thy", "line"="5") "definition \"bar = 1\""
end
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
