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