Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Display Draft in Jedit


view this post on Zulip Email Gateway (Aug 18 2022 at 19:47):

From: Christine Sherif Rizkallah <christine2711987@gmail.com>
Hi,

I'm wondering if anyone knows how to display drafts for isabelle files
opened in jedit?

Best,
Christine

view this post on Zulip Email Gateway (Aug 18 2022 at 19:47):

From: Makarius <makarius@sketis.net>
The Isabelle command for that is called 'display_drafts' as before,
although Proof General might have had a menu function for that.

Since Isabelle/jEdit still lacks first-class support for diagnostic
commands, one needs to type it carefully into the buffer; several
instances might pop up asynchronously due to continued editing.

Trying this myself on Linux, I now realize that an old Mac OS problem has
come back. Since PDF_VIEWER="xdg-open" is now the default on Linux, which
is asynchronous by itself, some extra workaround is needed. See
http://isabelle.in.tum.de/repos/isabelle-release/rev/21c42b095c84

Anyway, I rarely use display_drafts or print_drafts these days. The
Isabelle/jEdit buffer display quality with the IsabelleText font is
reasonable, and the standard Print function of jEdit does a surprisingly
good job for it. So in the long run, these latex-based draft commands
might well disappear -- I've had to repair them too many times over the
years.

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 19:48):

From: Peter Lammich <lammich@in.tum.de>
Have you tried typing the Isar-command
display_drafts "file-name"

Peter

view this post on Zulip Email Gateway (Aug 18 2022 at 19:48):

From: Christine Sherif Rizkallah <christine2711987@gmail.com>
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.

view this post on Zulip Email Gateway (Aug 18 2022 at 19:48):

From: Makarius <makarius@sketis.net>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 19:49):

From: Christine Sherif Rizkallah <christine2711987@gmail.com>
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


Last updated: Mar 29 2024 at 12:28 UTC