[isabelle-dev] document_output vs. old document_dump/document_dump_mode

[Tobias Nipkow]

Am 29/08/2012 14:21, schrieb Makarius:
> On Wed, 29 Aug 2012, Gerwin Klein wrote:
> 
>> A small annoyance with document_output was that the output doesn't seem to get
>> produced for document=false (i.e. seems to force a latex run) and that it
>> insists on creating a "document" subdirectory in the target directory that I
>> give it.
> 
> In fact it produces a sub-directory for each of the document_variants, which is
> just "document" by default.  The corresponding root.tex can be optionally
> prefixed by that name, too.  See afp/thys/Collections how it is used there to
> produce unrelated documents.
> 
> You can also short-circuit things by using a dummy root.tex with something like
> "touch roof.$FORMAT" in document/build, if you really need to run latex outside
> of the session context.  (I've never seen this situation in the conversions of
> old scripts in the past couple of weeks.)
> 
> So it is worth taking a fresh look at document_output -- it achieves more things
> with fewer options.

I am still having some problems with it. Given

session "HOL-IMP1" in "~~/src/HOL/IMP" = HOL +
  options [document_output="IMP-generated", document=pdf]
  theories
    BExp

then isabelle build -d . HOL-IMP1 puts IMP-generated into "~~/src/HOL/IMP" - I
guess that is to be expeced. But I want it in my current directory. This works

session "HOL-IMP1" in "~~/src/HOL/IMP" = HOL +
  options [document_output="$THIS_DIR/IMP-generated", document=pdf]
  theories
    BExp

but it requires me to set a shell variable THIS_DIR before invoking isabelle
build. Is there a more elegant way to achive the same effect?

I tried removing the "in":

session "HOL-IMP1" = HOL +
  options [document_output="IMP-generated", document=pdf]
  theories
     "~~/src/HOL/IMP/BExp"

But now I cannot find IMP-generated anywhere in my home directory. Where should
I look?

Thanks
Tobias