# HG changeset patch
# User wenzelm
# Date 1559390003 -7200
# Node ID 22c7eee0dd564d55e646dee32bb8901ead58f92d
# Parent  8dd987397e314a5c688132b1fc599b3c18fb0c7a# Parent  83774d669b5181fb28d19d7a0219fbf6c6d38aab
merged

diff -r 8dd987397e31 -r 22c7eee0dd56 .hgtags
--- a/.hgtags	Fri May 31 12:29:02 2019 +0200
+++ b/.hgtags	Sat Jun 01 13:53:23 2019 +0200
@@ -39,3 +39,4 @@
 9c60fcfdf495375cf1c886d7eb75583f63707950 Isabelle2019-RC1
 805250bb7363dbfcb072ed34bbfb522106bdd21a Isabelle2019-RC2
 85de4fdec61b4c19b5491e61b637b66ae247ef97 Isabelle2019-RC3
+ad2d84c4238064c72140763ea1fe4ab91a619d9e Isabelle2019-RC4
diff -r 8dd987397e31 -r 22c7eee0dd56 NEWS
--- a/NEWS	Fri May 31 12:29:02 2019 +0200
+++ b/NEWS	Sat Jun 01 13:53:23 2019 +0200
@@ -32,8 +32,8 @@
 feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
 via "isabelle update_cartouches -t" (available since Isabelle2015).
 
-* Infix operators that begin or end with a "*" can now be paranthesized
-without additional spaces, eg "(*)" instead of "( * )". Minor
+* Infix operators that begin or end with a "*" are now parenthesized
+without additional spaces, e.g. "(*)" instead of "( * )". Minor
 INCOMPATIBILITY.
 
 * Mixfix annotations may use cartouches instead of old-style double
@@ -256,7 +256,7 @@
 equation no longer tuples the arguments on the right-hand side.
 INCOMPATIBILITY.
 
-* Theory HOL-Library.Multiset: the <Union># operator now has the same
+* Theory HOL-Library.Multiset: the \<Union># operator now has the same
 precedence as any other prefix function symbol.
 
 * Theory HOL-Library.Cardinal_Notations has been discontinued in favor
diff -r 8dd987397e31 -r 22c7eee0dd56 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri May 31 12:29:02 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Jun 01 13:53:23 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.