merged
authorwenzelm
Wed Jan 20 19:19:55 2016 +0100 (2016-01-20 ago)
changeset 62215e208fa77beb1
parent 62209 009c6e0b44bb
parent 62214 451bd09b8277
child 62216 5fb86150a579
child 62225 c8c48906b858
merged
     1.1 --- a/Admin/components/components.sha1	Wed Jan 20 18:04:41 2016 +0100
     1.2 +++ b/Admin/components/components.sha1	Wed Jan 20 19:19:55 2016 +0100
     1.3 @@ -61,6 +61,7 @@
     1.4  c95ebf7777beb3e7ef10c0cf3f734cb78f9828e4  jdk-8u5.tar.gz
     1.5  74df343671deba03be7caa49de217d78b693f817  jdk-8u60.tar.gz
     1.6  dfb087bd64c3e5da79430e0ba706b9abc559c090  jdk-8u66.tar.gz
     1.7 +2ac389babd15aa5ddd1a424c1509e1c459e6fbb1  jdk-8u72.tar.gz
     1.8  44775a22f42a9d665696bfb49e53c79371c394b0  jedit_build-20111217.tar.gz
     1.9  a242a688810f2bccf24587b0062ce8027bf77fa2  jedit_build-20120304.tar.gz
    1.10  4c948dee53f74361c097c08f49a1a5ff9b17bd1d  jedit_build-20120307.tar.gz
     2.1 --- a/Admin/components/main	Wed Jan 20 18:04:41 2016 +0100
     2.2 +++ b/Admin/components/main	Wed Jan 20 19:19:55 2016 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  exec_process-1.0.3
     2.5  Haskabelle-2015
     2.6  isabelle_fonts-20160102
     2.7 -jdk-8u66
     2.8 +jdk-8u72
     2.9  jedit_build-20151124
    2.10  jfreechart-1.0.14-1
    2.11  jortho-1.0-2
     3.1 --- a/Admin/java/build	Wed Jan 20 18:04:41 2016 +0100
     3.2 +++ b/Admin/java/build	Wed Jan 20 19:19:55 2016 +0100
     3.3 @@ -14,8 +14,8 @@
     3.4  
     3.5  ## parameters
     3.6  
     3.7 -VERSION="8u66"
     3.8 -FULL_VERSION="1.8.0_66"
     3.9 +VERSION="8u72"
    3.10 +FULL_VERSION="1.8.0_72"
    3.11  
    3.12  ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
    3.13  ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
     4.1 --- a/src/Doc/JEdit/JEdit.thy	Wed Jan 20 18:04:41 2016 +0100
     4.2 +++ b/src/Doc/JEdit/JEdit.thy	Wed Jan 20 19:19:55 2016 +0100
     4.3 @@ -336,8 +336,7 @@
     4.4    in mind that this extra variance of GUI functionality is unlikely to work in
     4.5    arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close>
     4.6    should always work on all platforms, although they are technically and
     4.7 -  stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> on Linux should be
     4.8 -  ignored.
     4.9 +  stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
    4.10  
    4.11    After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>,
    4.12    Isabelle/jEdit should be restarted to take full effect.
     5.1 --- a/src/Pure/General/antiquote.ML	Wed Jan 20 18:04:41 2016 +0100
     5.2 +++ b/src/Pure/General/antiquote.ML	Wed Jan 20 19:19:55 2016 +0100
     5.3 @@ -79,7 +79,7 @@
     5.4  val scan_txt =
     5.5    Scan.repeats1
     5.6     (Scan.many1 (fn (s, _) =>
     5.7 -      not (Symbol.is_control s) andalso s <> "\\<open>" andalso s <> "@" andalso Symbol.not_eof s) ||
     5.8 +      not (Symbol.is_control s) andalso s <> Symbol.open_ andalso s <> "@" andalso Symbol.not_eof s) ||
     5.9      $$$ "@" --| Scan.ahead (~$$ "{"));
    5.10  
    5.11  val scan_antiq_body =
     6.1 --- a/src/Pure/General/pretty.ML	Wed Jan 20 18:04:41 2016 +0100
     6.2 +++ b/src/Pure/General/pretty.ML	Wed Jan 20 19:19:55 2016 +0100
     6.3 @@ -167,7 +167,7 @@
     6.4  val para = paragraph o text;
     6.5  
     6.6  fun quote prt = blk (1, [str "\"", prt, str "\""]);
     6.7 -fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
     6.8 +fun cartouche prt = blk (1, [str Symbol.open_, prt, str Symbol.close]);
     6.9  
    6.10  fun separate sep prts =
    6.11    flat (Library.separate [str sep, brk 1] (map single prts));
     7.1 --- a/src/Pure/General/symbol.ML	Wed Jan 20 18:04:41 2016 +0100
     7.2 +++ b/src/Pure/General/symbol.ML	Wed Jan 20 19:19:55 2016 +0100
     7.3 @@ -10,6 +10,8 @@
     7.4    val spaces: int -> string
     7.5    val STX: symbol
     7.6    val DEL: symbol
     7.7 +  val open_: symbol
     7.8 +  val close: symbol
     7.9    val space: symbol
    7.10    val comment: symbol
    7.11    val is_char: symbol -> bool
    7.12 @@ -93,6 +95,9 @@
    7.13  val STX = chr 2;
    7.14  val DEL = chr 127;
    7.15  
    7.16 +val open_ = "\\<open>";
    7.17 +val close = "\\<close>";
    7.18 +
    7.19  val space = chr 32;
    7.20  
    7.21  local
    7.22 @@ -115,7 +120,7 @@
    7.23    String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
    7.24  
    7.25  fun is_symbolic s =
    7.26 -  s <> "\\<open>" andalso s <> "\\<close>" andalso raw_symbolic s;
    7.27 +  s <> open_ andalso s <> close andalso raw_symbolic s;
    7.28  
    7.29  val is_symbolic_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
    7.30  
     8.1 --- a/src/Pure/General/symbol_pos.ML	Wed Jan 20 18:04:41 2016 +0100
     8.2 +++ b/src/Pure/General/symbol_pos.ML	Wed Jan 20 19:19:55 2016 +0100
     8.3 @@ -180,15 +180,15 @@
     8.4    Scan.repeat1 (Scan.depend (fn (depth: int option) =>
     8.5      (case depth of
     8.6        SOME d =>
     8.7 -        $$ "\\<open>" >> pair (SOME (d + 1)) ||
     8.8 +        $$ Symbol.open_ >> pair (SOME (d + 1)) ||
     8.9            (if d > 0 then
    8.10 -            Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair depth ||
    8.11 -            $$ "\\<close>" >> pair (if d = 1 then NONE else SOME (d - 1))
    8.12 +            Scan.one (fn (s, _) => s <> Symbol.close andalso Symbol.not_eof s) >> pair depth ||
    8.13 +            $$ Symbol.close >> pair (if d = 1 then NONE else SOME (d - 1))
    8.14            else Scan.fail)
    8.15      | NONE => Scan.fail)));
    8.16  
    8.17  fun scan_cartouche err_prefix =
    8.18 -  Scan.ahead ($$ "\\<open>") |--
    8.19 +  Scan.ahead ($$ Symbol.open_) |--
    8.20      !!! (fn () => err_prefix ^ "unclosed text cartouche")
    8.21        (Scan.provide is_none (SOME 0) scan_cartouche_depth);
    8.22  
     9.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jan 20 18:04:41 2016 +0100
     9.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jan 20 19:19:55 2016 +0100
     9.3 @@ -12,6 +12,7 @@
     9.4  
     9.5  import java.awt.{Color, Font, Toolkit, Window}
     9.6  import java.awt.event.KeyEvent
     9.7 +import java.awt.im.InputMethodRequests
     9.8  import javax.swing.JTextField
     9.9  import javax.swing.event.{DocumentListener, DocumentEvent}
    9.10  
    9.11 @@ -224,6 +225,8 @@
    9.12  
    9.13    /* key handling */
    9.14  
    9.15 +  override def getInputMethodRequests: InputMethodRequests = null
    9.16 +
    9.17    inputHandlerProvider =
    9.18      new DefaultInputHandlerProvider(new TextAreaInputHandler(text_area) {
    9.19        override def getAction(action: String): JEditBeanShellAction =