Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] display_drafts: printing the mupdf output


view this post on Zulip Email Gateway (Aug 19 2022 at 13:52):

From: Lawrence Paulson <lp15@cam.ac.uk>
I decided to see whether printing from jEdit worked under OS X or not. I encountered a lot of problems. Mostly they were because jEdit has its own print dialogue and ignores the built-in one.

JEdit’s print dialogue offered me a choice of printers, and the option of saving to a file. I chose a printer and selected the option, but the document was sent to the default printer instead, and no file was saved. Instead, jEdit went into a loop and had to be killed. So clearly something needs to be fixed here. (I tried both the last release and the current development version with the same results.)

On the other hand, the printed output itself is very attractive, nicer than that produced by the old display_drafts command. And of course it’s easier to simply choose “print” rather than enter a command. So I would happy to see display_drafts go, assuming of course that the OS X print dialogue problems can be fixed.

Larry

view this post on Zulip Email Gateway (Aug 19 2022 at 13:54):

From: Makarius <makarius@sketis.net>
On Thu, 27 Mar 2014, Lawrence Paulson wrote:

I decided to see whether printing from jEdit worked under OS X or not. I
encountered a lot of problems. Mostly they were because jEdit has its
own print dialogue and ignores the built-in one.

jEdit actually uses the regular print facility of Java. There were times
when Apple Java or early versions of Oracle Java on Mac OS X were crashing
on that in strange ways, but I did not encounter any problems recently.

Since Java 8 has been just release, we should revisit that soon, to see if
Oracle vs. Apple now works. I will come back to this on isabelle-dev,
when the first jdk-8 Isabelle component becomes available (maybe after the
next Java 8 release by Oracle).

JEdit’s print dialogue offered me a choice of printers, and the option
of saving to a file. I chose a printer and selected the option, but the
document was sent to the default printer instead, and no file was saved.

I can't remember that I've ever managed to "Print To File" with Java -- it
offers to write a PS file, which already looks suspicious. The way to go
is to let the printer driver produce a file for you. On Linux this works
via the cups-pdf mentioned before on this thread. On Mac OS X, I can't
tell on the spot.

This seems to be a standard Java question, unrelated to jEdit or
Isabelle/jEdit.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 13:54):

From: Lawrence Paulson <lp15@cam.ac.uk>
I installed this printer driver, and it launches, and appears to do something, but with no evident result.

An installation note states that outputs are written to the directory /opt/local/var/spool/cups-pdf/$USER. But I couldn’t find anything there.

Has anybody got jEdit printing to work under OS X?

Larry Paulson

view this post on Zulip Email Gateway (Aug 19 2022 at 13:56):

From: Fabian Immler <immler@in.tum.de>
I also run Mac OS X and jEdit sometimes seems to print to the default printer, regardless of the settings I chose.
If it manages to print to CUPS-pdf, I find the output in /Users/Shared/CUPS-PDF/$USER.

Fabian

view this post on Zulip Email Gateway (Aug 19 2022 at 13:56):

From: Makarius <makarius@sketis.net>
This does not sound too encouraging --- I did not expect Mac users
installing Unixoid tools to get basic functionality to work. What is also
a bit surprising is that nobody has reported any inconveniences about the
jEdit print function before, even though I keep advertizing it for 2-3
years. I am actually using it routinely on my Mac OS X Snow Leopard
(without cups-pdf), but did not know what a Mac user normally expects.

It is important to put problems on the table, with a clear problem
description and without speculations about "bugs" or "features".
Otherwise the situation will just just persist, and users continue
grumbling in some corner.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 13:59):

From: Holger Blasum <hbl@sysgo.com>
Dear Isabelle users,

it's a fine weather today at my place and I'd like to print out
some paper copies with display_drafts. However, invoking
display_drafts invokes mupdf which nicely display PDFs but
I don't figure out how to send this to a printer (or at least
get some postscript of PDF from it), and I don't
see any printing support in a very sketchy look at
http://git.ghostscript.com/?p=mupdf.git;a=blob;f=source/tools/pdfshow.c;h=c5d021ad07777264ca8c7379e7450e458d7b88b2;hb=HEAD
:-(

If I look into my process list (ps aux, the operating system
"mupdf /tmp/isabelle-hbl12562/13122document1623991.pdf"
but it this file is immediately deleted after being sent
to mupdf :-( Of course I could capture screenshots or set up
the "proper" document generation (via "isabelle build") but I'm
wondering whether there is a more elegant way.

thx,

view this post on Zulip Email Gateway (Aug 19 2022 at 13:59):

From: Holger Blasum <hbl@sysgo.com>
FWIW: the workaround I finally chose was
"ln -s /usr/local/xpdf /usr/local/bin/mupdf"

view this post on Zulip Email Gateway (Aug 19 2022 at 13:59):

From: Makarius <makarius@sketis.net>
The display_drafts command invokes the command-line tool "isabelle
display" (which is explained further in the system manual). In particular
the Isabelle settings variable PDF_VIEWER tells how to display the pdf.
By default this is delegated to the desktop environment, on Linux via
xdg-open and similar commands on the other plaforms (where this usually
works even better).

Just today, I've asked myself if it is now time to discontine
display_drafts. It was introduced 10 years ago as workaroud for
Emacs-based Proof General, since printing of text buffers did not quite
work back then, especially with what was still X-Symbol at that time.

Isabelle/jEdit shows text via the Unicode rendering of Isabelle symbols,
with IsabelleText font. Both of that together gives surprisingly good
results with the regular File / Print operation of the editor.

So ar there any compelling reasons to continue maintaining the
display_drafts command, which had to be repaired numerous times in the
past and does not even work out of the box on most platforms (due to lack
of proper latex setup)?

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 14:06):

From: Holger Blasum <hbl@sysgo.com>
On 03-10, Makarius wrote:

On Sun, 9 Mar 2014, Holger Blasum wrote:
Just today, I've asked myself if it is now time to discontine
display_drafts. It was introduced 10 years ago as workaroud for
Emacs-based Proof General, since printing of text buffers did not
quite work back then, especially with what was still X-Symbol at
that time.

Isabelle/jEdit shows text via the Unicode rendering of Isabelle
symbols, with IsabelleText font. Both of that together gives
surprisingly good results with the regular File / Print operation of
the editor.

Having tried out printing from Isabelle/jEdit today, I would
agree that at least personally I can go with printing from jEdit
(for PDF generation, I did not spot an explicit jEdit option,
but printing to the PDF printer driver obtained by "sudo apt-get install
cups-pdf" does the job as well).

So ar there any compelling reasons to continue maintaining the
display_drafts command, which had to be repaired numerous times in
the past and does not even work out of the box on most platforms
(due to lack of proper latex setup)?

br,

view this post on Zulip Email Gateway (Aug 19 2022 at 14:06):

From: Makarius <makarius@sketis.net>
I am using the same cups-pdf on Linux, which I did not know before my
first attempt of printing with jEdit. I found the quality of both
surprisingly high, so that is a win-win situation.

Nonetheless there is still an opportunity to point out important uses of
the old 'display_drafts' command. If nothing happens, I will remove it
for the coming release (summer 2014).

Makarius


Last updated: Apr 20 2024 at 12:26 UTC