hint on printing via Web browser; Isabelle2019-RC4
authorwenzelm
Sat Jun 01 11:27:19 2019 +0200 (6 weeks ago)
changeset 70298ad2d84c42380
parent 70297 67edf0234417
child 70299 83774d669b51
hint on printing via Web browser;
src/Doc/JEdit/JEdit.thy
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Tue May 28 19:52:14 2019 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Sat Jun 01 11:27:19 2019 +0200
     1.3 @@ -1954,7 +1954,7 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 -section \<open>Document preview \label{sec:document-preview}\<close>
     1.8 +section \<open>Document preview and printing \label{sec:document-preview}\<close>
     1.9  
    1.10  text \<open>
    1.11    The action @{action_def isabelle.preview} opens an HTML preview of the
    1.12 @@ -1964,6 +1964,10 @@
    1.13  
    1.14    Action @{action_def isabelle.draft} is similar to @{action
    1.15    isabelle.preview}, but shows a plain-text document draft.
    1.16 +
    1.17 +  Both actions show document sources in a regular Web browser, which may be
    1.18 +  also used to print the result in a more portable manner than the Java
    1.19 +  printer dialog of the jEdit @{action_ref print} action.
    1.20  \<close>
    1.21  
    1.22  
    1.23 @@ -2185,6 +2189,11 @@
    1.24  
    1.25    \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>Isabelle DejaVu\<close> fonts.
    1.26  
    1.27 +  \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X the Java printer dialog sometimes does not work.
    1.28 +
    1.29 +  \<^bold>\<open>Workaround:\<close> Use action @{action isabelle.draft} and print via the Web
    1.30 +  browser.
    1.31 +
    1.32    \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
    1.33    event handling of Java/AWT/Swing.
    1.34