Re: [isabelle] Display Draft in Jedit

Works, thanks!
Apparently I just have to always write the complete path (even if I'm at
the file I want to display draft for).


On Sun, May 20, 2012 at 10:03 PM, Makarius <makarius at> wrote:

> On Sun, 20 May 2012, Christine Sherif Rizkallah wrote:
>  I tried display_drafts "file-name".
>> I get the error "Bad file name: file-name". I'm using a Mac, maybe that is
>> the problem.
> The Mac is often a problem, but probably not this time.  The following
> should work
>  display_drafts "~~/src/HOL/ex/Seq.thy"
> assuming that you have LaTeX installed.
>        Makarius

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