--- a/Admin/components/components.sha1 Wed Jan 20 18:04:41 2016 +0100
+++ b/Admin/components/components.sha1 Wed Jan 20 19:19:55 2016 +0100
@@ -61,6 +61,7 @@
c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4 jdk-8u5.tar.gz
74df343671deba03be7caa49de217d78b693f817 jdk-8u60.tar.gz
dfb087bd64c3e5da79430e0ba706b9abc559c090 jdk-8u66.tar.gz
+2ac389babd15aa5ddd1a424c1509e1c459e6fbb1 jdk-8u72.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Wed Jan 20 18:04:41 2016 +0100
+++ b/Admin/components/main Wed Jan 20 19:19:55 2016 +0100
@@ -5,7 +5,7 @@
exec_process-1.0.3
Haskabelle-2015
isabelle_fonts-20160102
-jdk-8u66
+jdk-8u72
jedit_build-20151124
jfreechart-1.0.14-1
jortho-1.0-2
--- a/Admin/java/build Wed Jan 20 18:04:41 2016 +0100
+++ b/Admin/java/build Wed Jan 20 19:19:55 2016 +0100
@@ -14,8 +14,8 @@
## parameters
-VERSION="8u66"
-FULL_VERSION="1.8.0_66"
+VERSION="8u72"
+FULL_VERSION="1.8.0_72"
ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
--- a/src/Doc/JEdit/JEdit.thy Wed Jan 20 18:04:41 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy Wed Jan 20 19:19:55 2016 +0100
@@ -336,8 +336,7 @@
in mind that this extra variance of GUI functionality is unlikely to work in
arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close>
should always work on all platforms, although they are technically and
- stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> on Linux should be
- ignored.
+ stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>,
Isabelle/jEdit should be restarted to take full effect.
--- a/src/Pure/General/antiquote.ML Wed Jan 20 18:04:41 2016 +0100
+++ b/src/Pure/General/antiquote.ML Wed Jan 20 19:19:55 2016 +0100
@@ -79,7 +79,7 @@
val scan_txt =
Scan.repeats1
(Scan.many1 (fn (s, _) =>
- not (Symbol.is_control s) andalso s <> "\\<open>" andalso s <> "@" andalso Symbol.not_eof s) ||
+ not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso Symbol.not_eof s) ||
$$$ "@" --| Scan.ahead (~$$ "{"));
val scan_antiq_body =
--- a/src/Pure/General/pretty.ML Wed Jan 20 18:04:41 2016 +0100
+++ b/src/Pure/General/pretty.ML Wed Jan 20 19:19:55 2016 +0100
@@ -167,7 +167,7 @@
val para = paragraph o text;
fun quote prt = blk (1, [str "\"", prt, str "\""]);
-fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
+fun cartouche prt = blk (1, [str Symbol.open_, prt, str Symbol.close]);
fun separate sep prts =
flat (Library.separate [str sep, brk 1] (map single prts));
--- a/src/Pure/General/symbol.ML Wed Jan 20 18:04:41 2016 +0100
+++ b/src/Pure/General/symbol.ML Wed Jan 20 19:19:55 2016 +0100
@@ -10,6 +10,8 @@
val spaces: int -> string
val STX: symbol
val DEL: symbol
+ val open_: symbol
+ val close: symbol
val space: symbol
val comment: symbol
val is_char: symbol -> bool
@@ -93,6 +95,9 @@
val STX = chr 2;
val DEL = chr 127;
+val open_ = "\\<open>";
+val close = "\\<close>";
+
val space = chr 32;
local
@@ -115,7 +120,7 @@
String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
fun is_symbolic s =
- s <> "\\<open>" andalso s <> "\\<close>" andalso raw_symbolic s;
+ s <> open_ andalso s <> close andalso raw_symbolic s;
val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
--- a/src/Pure/General/symbol_pos.ML Wed Jan 20 18:04:41 2016 +0100
+++ b/src/Pure/General/symbol_pos.ML Wed Jan 20 19:19:55 2016 +0100
@@ -180,15 +180,15 @@
Scan.repeat1 (Scan.depend (fn (depth: int option) =>
(case depth of
SOME d =>
- $$ "\\<open>" >> pair (SOME (d + 1)) ||
+ $$ Symbol.open_ >> pair (SOME (d + 1)) ||
(if d > 0 then
- Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair depth ||
- $$ "\\<close>" >> pair (if d = 1 then NONE else SOME (d - 1))
+ Scan.one (fn (s, _) => s <> Symbol.close andalso Symbol.not_eof s) >> pair depth ||
+ $$ Symbol.close >> pair (if d = 1 then NONE else SOME (d - 1))
else Scan.fail)
| NONE => Scan.fail)));
fun scan_cartouche err_prefix =
- Scan.ahead ($$ "\\<open>") |--
+ Scan.ahead ($$ Symbol.open_) |--
!!! (fn () => err_prefix ^ "unclosed text cartouche")
(Scan.provide is_none (SOME 0) scan_cartouche_depth);
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Jan 20 18:04:41 2016 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Jan 20 19:19:55 2016 +0100
@@ -12,6 +12,7 @@
import java.awt.{Color, Font, Toolkit, Window}
import java.awt.event.KeyEvent
+import java.awt.im.InputMethodRequests
import javax.swing.JTextField
import javax.swing.event.{DocumentListener, DocumentEvent}
@@ -224,6 +225,8 @@
/* key handling */
+ override def getInputMethodRequests: InputMethodRequests = null
+
inputHandlerProvider =
new DefaultInputHandlerProvider(new TextAreaInputHandler(text_area) {
override def getAction(action: String): JEditBeanShellAction =