Re: [isabelle] Easier quick PDF generation possible?



Joachim, all,

Gets +1 from me !

Regards, Andrew

On 23 Oct 2014, at 12:44, Joachim Breitner <breitner at kit.edu> wrote:

> 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

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero at TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                          http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------





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