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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev