--- a/Admin/PLATFORMS Mon Nov 23 17:00:32 2015 +0000
+++ b/Admin/PLATFORMS Mon Nov 23 21:55:13 2015 +0100
@@ -33,10 +33,10 @@
x86-linux Ubuntu 10.04 LTS
x86_64-linux Ubuntu 10.04 LTS
- x86_64-darwin Mac OS X 10.7 Lion (macbroy6)
- Mac OS X 10.8 Mountain Lion (macbroy30)
+ x86_64-darwin Mac OS X 10.8 Mountain Lion (macbroy30)
Mac OS X 10.9 Mavericks (macbroy2)
Mac OS X 10.10 Yosemite (macbroy31)
+ Mac OS X 10.11 El Capitan
x86-cygwin Cygwin 1.7 (vmbroy9)
--- a/Admin/components/components.sha1 Mon Nov 23 17:00:32 2015 +0000
+++ b/Admin/components/components.sha1 Mon Nov 23 21:55:13 2015 +0100
@@ -104,6 +104,7 @@
b4b624fb5f34d1dc814fb4fb469fafd7d7ea018a polyml-5.5.3-20150908.tar.gz
b668e1f43a41608a8eb365c5e19db6c54c72748a polyml-5.5.3-20150911.tar.gz
1f5cd9b1390dab13861f90dfc06d4180cc107587 polyml-5.5.3-20150916.tar.gz
+03ba81e595fa6d6df069532d67ad3195c37d9046 polyml-5.6-20151123.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz
--- a/Admin/components/main Mon Nov 23 17:00:32 2015 +0000
+++ b/Admin/components/main Mon Nov 23 21:55:13 2015 +0100
@@ -10,7 +10,7 @@
jfreechart-1.0.14-1
jortho-1.0-2
kodkodi-1.5.2
-polyml-5.5.3-20150916
+polyml-5.6-20151123
scala-2.11.7
spass-3.8ds
xz-java-1.2-1
--- a/Admin/polyml/README Mon Nov 23 17:00:32 2015 +0000
+++ b/Admin/polyml/README Mon Nov 23 21:55:13 2015 +0100
@@ -1,8 +1,8 @@
Poly/ML for Isabelle
====================
-This is a preview of Poly/ML 5.5.3, based on
-https://github.com/polyml/polyml/
+This is a preview of Poly/ML 5.6, based on
+https://github.com/polyml/polyml/ commit b49eb17ab516.
The included build script is used like this:
@@ -18,4 +18,4 @@
Makarius
- 31-Aug-2015
+ 23-Nov-2015
--- a/Admin/polyml/settings Mon Nov 23 17:00:32 2015 +0000
+++ b/Admin/polyml/settings Mon Nov 23 21:55:13 2015 +0100
@@ -41,7 +41,7 @@
# ML settings
- ML_SYSTEM=polyml-5.5.3
+ ML_SYSTEM=polyml-5.6
ML_PLATFORM="$PLATFORM"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_SOURCES="$POLYML_HOME/src"
--- a/src/Pure/GUI/gui.scala Mon Nov 23 17:00:32 2015 +0000
+++ b/src/Pure/GUI/gui.scala Mon Nov 23 21:55:13 2015 +0100
@@ -215,6 +215,10 @@
/* font operations */
+ def copy_font(font: Font): Font =
+ if (font == null) null
+ else new Font(font.getFamily, font.getStyle, font.getSize)
+
def line_metrics(font: Font): LineMetrics =
font.getLineMetrics("", new FontRenderContext(null, false, false))
--- a/src/Tools/jEdit/src/jedit_options.scala Mon Nov 23 17:00:32 2015 +0000
+++ b/src/Tools/jEdit/src/jedit_options.scala Mon Nov 23 21:55:13 2015 +0100
@@ -88,11 +88,10 @@
def save = bool(opt_name) = selected
}
else {
- val default_font = UIManager.getFont("TextField.font")
+ val default_font = GUI.copy_font(UIManager.getFont("TextField.font"))
val text_area =
new TextArea with Option_Component {
- if (default_font != null) font =
- new Font(default_font.getFamily, default_font.getStyle, default_font.getSize)
+ if (default_font != null) font = default_font
name = opt_name
val title = opt_title
def load = text = value.check_name(opt_name).value
--- a/src/Tools/jEdit/src/session_build.scala Mon Nov 23 17:00:32 2015 +0000
+++ b/src/Tools/jEdit/src/session_build.scala Mon Nov 23 21:55:13 2015 +0100
@@ -45,7 +45,7 @@
columns = 65
rows = 24
}
- text.font = (new Label).font
+ text.font = GUI.copy_font((new Label).font)
private val scroll_text = new ScrollPane(text)