# HG changeset patch
# User wenzelm
# Date 1559381239 -7200
# Node ID ad2d84c4238064c72140763ea1fe4ab91a619d9e
# Parent  67edf0234417204a0985a766d840b365c33a5f04
hint on printing via Web browser;

diff -r 67edf0234417 -r ad2d84c42380 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Tue May 28 19:52:14 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Jun 01 11:27:19 2019 +0200
@@ -1954,7 +1954,7 @@
 \<close>
 
 
-section \<open>Document preview \label{sec:document-preview}\<close>
+section \<open>Document preview and printing \label{sec:document-preview}\<close>
 
 text \<open>
   The action @{action_def isabelle.preview} opens an HTML preview of the
@@ -1964,6 +1964,10 @@
 
   Action @{action_def isabelle.draft} is similar to @{action
   isabelle.preview}, but shows a plain-text document draft.
+
+  Both actions show document sources in a regular Web browser, which may be
+  also used to print the result in a more portable manner than the Java
+  printer dialog of the jEdit @{action_ref print} action.
 \<close>
 
 
@@ -2185,6 +2189,11 @@
 
   \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>Isabelle DejaVu\<close> fonts.
 
+  \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X the Java printer dialog sometimes does not work.
+
+  \<^bold>\<open>Workaround:\<close> Use action @{action isabelle.draft} and print via the Web
+  browser.
+
   \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
   event handling of Java/AWT/Swing.