misc tuning to accomodate scala-2.10.0-M2;
authorwenzelm
Sat, 17 Mar 2012 17:44:29 +0100
changeset 47868395b7277ed76
parent 47867 f1856425224e
child 47869 11b38c94b21a
misc tuning to accomodate scala-2.10.0-M2;
src/Pure/General/symbol.scala
src/Pure/PIDE/document.scala
src/Pure/library.scala
src/Tools/jEdit/README_BUILD
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/General/symbol.scala	Sat Mar 17 17:36:10 2012 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Sat Mar 17 17:44:29 2012 +0100
     1.3 @@ -267,13 +267,13 @@
     1.4        val mapping =
     1.5          for {
     1.6            (sym, props) <- symbols
     1.7 -          val code =
     1.8 +          code =
     1.9              try { Integer.decode(props("code")).intValue }
    1.10              catch {
    1.11                case _: NoSuchElementException => error("Missing code for symbol " + sym)
    1.12                case _: NumberFormatException => error("Bad code for symbol " + sym)
    1.13              }
    1.14 -          val ch = new String(Character.toChars(code))
    1.15 +          ch = new String(Character.toChars(code))
    1.16          } yield {
    1.17            if (code < 128) error("Illegal ASCII code for symbol " + sym)
    1.18            else (sym, ch)
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Mar 17 17:36:10 2012 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Mar 17 17:44:29 2012 +0100
     2.3 @@ -467,7 +467,7 @@
     2.4        var execs1 = Map.empty[Exec_ID, Command.State]
     2.5        for {
     2.6          (version_id, version) <- versions1.iterator
     2.7 -        val command_execs = assignments1(version_id).command_execs
     2.8 +        command_execs = assignments1(version_id).command_execs
     2.9          (_, node) <- version.nodes.entries
    2.10          command <- node.commands.iterator
    2.11        } {
     3.1 --- a/src/Pure/library.scala	Sat Mar 17 17:36:10 2012 +0100
     3.2 +++ b/src/Pure/library.scala	Sat Mar 17 17:44:29 2012 +0100
     3.3 @@ -130,8 +130,8 @@
     3.4  
     3.5    /* simple dialogs */
     3.6  
     3.7 -  private def simple_dialog(kind: Int, default_title: String)
     3.8 -    (parent: Component, title: String, message: Any*)
     3.9 +  private def simple_dialog(kind: Int, default_title: String,
    3.10 +    parent: Component, title: String, message: Seq[Any])
    3.11    {
    3.12      Swing_Thread.now {
    3.13        val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
    3.14 @@ -141,9 +141,14 @@
    3.15      }
    3.16    }
    3.17  
    3.18 -  def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
    3.19 -  def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
    3.20 -  def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
    3.21 +  def dialog(parent: Component, title: String, message: Any*) =
    3.22 +    simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
    3.23 +
    3.24 +  def warning_dialog(parent: Component, title: String, message: Any*) =
    3.25 +    simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
    3.26 +
    3.27 +  def error_dialog(parent: Component, title: String, message: Any*) =
    3.28 +    simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
    3.29  
    3.30    def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
    3.31      Swing_Thread.now {
     4.1 --- a/src/Tools/jEdit/README_BUILD	Sat Mar 17 17:36:10 2012 +0100
     4.2 +++ b/src/Tools/jEdit/README_BUILD	Sat Mar 17 17:44:29 2012 +0100
     4.3 @@ -9,6 +9,8 @@
     4.4  * Scala 2.8.2.final or 2.9.1-1
     4.5    http://www.scala-lang.org
     4.6  
     4.7 +  (experimental support for Scala 2.10.x milestones)
     4.8 +
     4.9  * Auxiliary jedit_build component
    4.10    http://www4.in.tum.de/~wenzelm/test/jedit_build-20120313.tar.gz
    4.11  
     5.1 --- a/src/Tools/jEdit/src/document_view.scala	Sat Mar 17 17:36:10 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sat Mar 17 17:44:29 2012 +0100
     5.3 @@ -124,10 +124,10 @@
     5.4      Text.Perspective(
     5.5        for {
     5.6          i <- 0 until text_area.getVisibleLines
     5.7 -        val start = text_area.getScreenLineStartOffset(i)
     5.8 -        val stop = text_area.getScreenLineEndOffset(i)
     5.9 +        start = text_area.getScreenLineStartOffset(i)
    5.10 +        stop = text_area.getScreenLineEndOffset(i)
    5.11          if start >= 0 && stop >= 0
    5.12 -        val range <- buffer_range.try_restrict(Text.Range(start, stop))
    5.13 +        range <- buffer_range.try_restrict(Text.Range(start, stop))
    5.14          if !range.is_singularity
    5.15        }
    5.16        yield range)
    5.17 @@ -388,10 +388,10 @@
    5.18                        if (visible_cmds.exists(changed.commands)) {
    5.19                          for {
    5.20                            line <- 0 until text_area.getVisibleLines
    5.21 -                          val start = text_area.getScreenLineStartOffset(line) if start >= 0
    5.22 -                          val end = text_area.getScreenLineEndOffset(line) if end >= 0
    5.23 -                          val range = proper_line_range(start, end)
    5.24 -                          val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    5.25 +                          start = text_area.getScreenLineStartOffset(line) if start >= 0
    5.26 +                          end = text_area.getScreenLineEndOffset(line) if end >= 0
    5.27 +                          range = proper_line_range(start, end)
    5.28 +                          line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
    5.29                            if line_cmds.exists(changed.commands)
    5.30                          } text_area.invalidateScreenLineRange(line, line)
    5.31                        }
     6.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Mar 17 17:36:10 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Mar 17 17:44:29 2012 +0100
     6.3 @@ -181,7 +181,7 @@
     6.4    def document_views(buffer: Buffer): List[Document_View] =
     6.5      for {
     6.6        text_area <- jedit_text_areas(buffer).toList
     6.7 -      val doc_view = document_view(text_area)
     6.8 +      doc_view = document_view(text_area)
     6.9        if doc_view.isDefined
    6.10      } yield doc_view.get
    6.11