merged
authorwenzelm
Sat Jun 01 13:53:23 2019 +0200 (4 months ago)
changeset 7030022c7eee0dd56
parent 70296 8dd987397e31
parent 70299 83774d669b51
child 70301 9f2a6856b912
merged
NEWS
     1.1 --- a/.hgtags	Fri May 31 12:29:02 2019 +0200
     1.2 +++ b/.hgtags	Sat Jun 01 13:53:23 2019 +0200
     1.3 @@ -39,3 +39,4 @@
     1.4  9c60fcfdf495375cf1c886d7eb75583f63707950 Isabelle2019-RC1
     1.5  805250bb7363dbfcb072ed34bbfb522106bdd21a Isabelle2019-RC2
     1.6  85de4fdec61b4c19b5491e61b637b66ae247ef97 Isabelle2019-RC3
     1.7 +ad2d84c4238064c72140763ea1fe4ab91a619d9e Isabelle2019-RC4
     2.1 --- a/NEWS	Fri May 31 12:29:02 2019 +0200
     2.2 +++ b/NEWS	Sat Jun 01 13:53:23 2019 +0200
     2.3 @@ -32,8 +32,8 @@
     2.4  feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
     2.5  via "isabelle update_cartouches -t" (available since Isabelle2015).
     2.6  
     2.7 -* Infix operators that begin or end with a "*" can now be paranthesized
     2.8 -without additional spaces, eg "(*)" instead of "( * )". Minor
     2.9 +* Infix operators that begin or end with a "*" are now parenthesized
    2.10 +without additional spaces, e.g. "(*)" instead of "( * )". Minor
    2.11  INCOMPATIBILITY.
    2.12  
    2.13  * Mixfix annotations may use cartouches instead of old-style double
    2.14 @@ -256,7 +256,7 @@
    2.15  equation no longer tuples the arguments on the right-hand side.
    2.16  INCOMPATIBILITY.
    2.17  
    2.18 -* Theory HOL-Library.Multiset: the <Union># operator now has the same
    2.19 +* Theory HOL-Library.Multiset: the \<Union># operator now has the same
    2.20  precedence as any other prefix function symbol.
    2.21  
    2.22  * Theory HOL-Library.Cardinal_Notations has been discontinued in favor
     3.1 --- a/src/Doc/JEdit/JEdit.thy	Fri May 31 12:29:02 2019 +0200
     3.2 +++ b/src/Doc/JEdit/JEdit.thy	Sat Jun 01 13:53:23 2019 +0200
     3.3 @@ -1954,7 +1954,7 @@
     3.4  \<close>
     3.5  
     3.6  
     3.7 -section \<open>Document preview \label{sec:document-preview}\<close>
     3.8 +section \<open>Document preview and printing \label{sec:document-preview}\<close>
     3.9  
    3.10  text \<open>
    3.11    The action @{action_def isabelle.preview} opens an HTML preview of the
    3.12 @@ -1964,6 +1964,10 @@
    3.13  
    3.14    Action @{action_def isabelle.draft} is similar to @{action
    3.15    isabelle.preview}, but shows a plain-text document draft.
    3.16 +
    3.17 +  Both actions show document sources in a regular Web browser, which may be
    3.18 +  also used to print the result in a more portable manner than the Java
    3.19 +  printer dialog of the jEdit @{action_ref print} action.
    3.20  \<close>
    3.21  
    3.22  
    3.23 @@ -2185,6 +2189,11 @@
    3.24  
    3.25    \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>Isabelle DejaVu\<close> fonts.
    3.26  
    3.27 +  \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X the Java printer dialog sometimes does not work.
    3.28 +
    3.29 +  \<^bold>\<open>Workaround:\<close> Use action @{action isabelle.draft} and print via the Web
    3.30 +  browser.
    3.31 +
    3.32    \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
    3.33    event handling of Java/AWT/Swing.
    3.34