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).

Christine

On Sun, May 20, 2012 at 10:03 PM, Makarius <makarius at sketis.net> 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.