Email Gateway (Aug 18 2022 at 19:47): 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
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
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
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.
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
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: Nov 21 2024 at 12:39 UTC