[isabelle-dev] Mirabelle and load path

[Makarius]

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.


 	Makarius
-------------- next part --------------
theory 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