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