# HG changeset patch # User wenzelm # Date 1453313995 -3600 # Node ID e208fa77beb1eb71251ffddbf4129dfd8aea21d0 # Parent 009c6e0b44bba78292d689ee24da0bbf287ac5d0# Parent 451bd09b8277d2e65c626168fc618f22141f9ca1 merged diff -r 009c6e0b44bb -r e208fa77beb1 Admin/components/components.sha1 --- 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 diff -r 009c6e0b44bb -r e208fa77beb1 Admin/components/main --- 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 diff -r 009c6e0b44bb -r e208fa77beb1 Admin/java/build --- 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" diff -r 009c6e0b44bb -r e208fa77beb1 src/Doc/JEdit/JEdit.thy --- 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>\Metal\ and \<^emph>\Nimbus\ should always work on all platforms, although they are technically and - stylistically outdated. The historic \<^emph>\CDE/Motif\ on Linux should be - ignored. + stylistically outdated. The historic \<^emph>\CDE/Motif\ should be ignored. After changing the look-and-feel in \<^emph>\Global Options~/ Appearance\, Isabelle/jEdit should be restarted to take full effect. diff -r 009c6e0b44bb -r e208fa77beb1 src/Pure/General/antiquote.ML --- 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 <> "\\" 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 = diff -r 009c6e0b44bb -r e208fa77beb1 src/Pure/General/pretty.ML --- 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 "\\", prt, str "\\"]); +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)); diff -r 009c6e0b44bb -r e208fa77beb1 src/Pure/General/symbol.ML --- 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_ = "\\"; +val 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 <> "\\" andalso s <> "\\" andalso raw_symbolic s; + s <> open_ andalso s <> close andalso raw_symbolic s; val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~"); diff -r 009c6e0b44bb -r e208fa77beb1 src/Pure/General/symbol_pos.ML --- 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 => - $$ "\\" >> pair (SOME (d + 1)) || + $$ Symbol.open_ >> pair (SOME (d + 1)) || (if d > 0 then - Scan.one (fn (s, _) => s <> "\\" andalso Symbol.not_eof s) >> pair depth || - $$ "\\" >> 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 ($$ "\\") |-- + Scan.ahead ($$ Symbol.open_) |-- !!! (fn () => err_prefix ^ "unclosed text cartouche") (Scan.provide is_none (SOME 0) scan_cartouche_depth); diff -r 009c6e0b44bb -r e208fa77beb1 src/Tools/jEdit/src/pretty_text_area.scala --- 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 =