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