# [isabelle] Problem with isatool usedir -V

• To: cl-isabelle-users at lists.cam.ac.uk
• Subject: [isabelle] Problem with isatool usedir -V
• From: Nicole Rauch <rauch at informatik.uni-kl.de>
• Date: Thu, 6 Oct 2005 09:15:45 +0200
• References: <8585D309-4E7F-4200-9AAA-C8B243F7185B@informatik.uni-kl.de> <Pine.LNX.4.58.0509291735290.16817@atbroy10.informatik.tu-muenchen.de>

```Hello,

```
thanks for the pointers to the -V switch, it is indeed very nice. But for me, it does not work properly out-of-the-box:
```
I'm using the cmdline

```
USEDIR = \$(ISATOOL) usedir -C true -v true -i true -d pdf -g true -p 0 -D document -V document=-proof,-ML
```
```
and it generates a document.pdf and outline.pdf in my ~/isabelle/ directory. But these files contain nothing but the header lines. I.e. I get the correct number of pages, but they are all blank except the header lines (generated by fancyheadings). I found this quite strange but did not care too much because I rather like to compile the resulting report in my original directory "document", as specified with -D. But there, it would only generate the full report. After some investigation I guess it must be the case that isabelletags.sty (which seems to be responsible for setting the appropriate \isakeeptag and \isadroptag commands for the desired version) is not copied over to the "document" directory. I've now set the desired commands in my root.tex, so now it works fine for me, but I found this quite counter-intuitive. Maybe somebody could tell me why the pages are blank in document.pdf and in outline.pdf and why the isabelletags.sty is not copied over?
```
Regards,

Nicole

--
"Never in the field of software development was so much owed by so
```
many to so few lines of code" -- Martin Fowler about JUnit
```
```

Attachment: PGP.sig
Description: Signierter Teil der Nachricht

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.