[isabelle] Easier quick PDF generation possible?



Hi,

I just create a small theory to do a quick experiment, and I wanted to
share it with someone. Isabelle can create pretty PDF output, so I
wanted to share it as such, but this turns out to be a task that is
unnecessary complicated.

Here is my log:

1. run "isabelle mkroot"
2. notice that I ran it wrong, "rm ROOT"
3. run "isabelle mkroot -d"
4. add my theory to ROOT, removed the theories [document = false]
   section, because empty sections are not allowed
5. run "isabelle build -D"
6. noticed that a few other theories were pulled in that I did not want
7. tried to add their theory names to the [document = false] section,
   for which I first had to look up the syntax in another ROOT file
8. noticed that this did not work. Put in the theory path (i.e. 
   "~~/src/HOL/Library/Extended_Real") in there
9. adjusted document/root.txt to have a proper title and not disclose my
   local username

Here is what I would have liked to do:

1. run "isabelle thy2pdf Foo.thy"


So if anyone agrees that this would be useful, and is able to implement
this minor feature suggestion, I’d appreciate that!

Thanks,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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