--- a/src/Pure/General/symbol.scala Sat Mar 17 17:36:10 2012 +0100
+++ b/src/Pure/General/symbol.scala Sat Mar 17 17:44:29 2012 +0100
@@ -267,13 +267,13 @@
val mapping =
for {
(sym, props) <- symbols
- val code =
+ code =
try { Integer.decode(props("code")).intValue }
catch {
case _: NoSuchElementException => error("Missing code for symbol " + sym)
case _: NumberFormatException => error("Bad code for symbol " + sym)
}
- val ch = new String(Character.toChars(code))
+ ch = new String(Character.toChars(code))
} yield {
if (code < 128) error("Illegal ASCII code for symbol " + sym)
else (sym, ch)
--- a/src/Pure/PIDE/document.scala Sat Mar 17 17:36:10 2012 +0100
+++ b/src/Pure/PIDE/document.scala Sat Mar 17 17:44:29 2012 +0100
@@ -467,7 +467,7 @@
var execs1 = Map.empty[Exec_ID, Command.State]
for {
(version_id, version) <- versions1.iterator
- val command_execs = assignments1(version_id).command_execs
+ command_execs = assignments1(version_id).command_execs
(_, node) <- version.nodes.entries
command <- node.commands.iterator
} {
--- a/src/Pure/library.scala Sat Mar 17 17:36:10 2012 +0100
+++ b/src/Pure/library.scala Sat Mar 17 17:44:29 2012 +0100
@@ -130,8 +130,8 @@
/* simple dialogs */
- private def simple_dialog(kind: Int, default_title: String)
- (parent: Component, title: String, message: Any*)
+ private def simple_dialog(kind: Int, default_title: String,
+ parent: Component, title: String, message: Seq[Any])
{
Swing_Thread.now {
val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
@@ -141,9 +141,14 @@
}
}
- def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
- def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
- def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
+ def dialog(parent: Component, title: String, message: Any*) =
+ simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
+
+ def warning_dialog(parent: Component, title: String, message: Any*) =
+ simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
+
+ def error_dialog(parent: Component, title: String, message: Any*) =
+ simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
Swing_Thread.now {
--- a/src/Tools/jEdit/README_BUILD Sat Mar 17 17:36:10 2012 +0100
+++ b/src/Tools/jEdit/README_BUILD Sat Mar 17 17:44:29 2012 +0100
@@ -9,6 +9,8 @@
* Scala 2.8.2.final or 2.9.1-1
http://www.scala-lang.org
+ (experimental support for Scala 2.10.x milestones)
+
* Auxiliary jedit_build component
http://www4.in.tum.de/~wenzelm/test/jedit_build-20120313.tar.gz
--- a/src/Tools/jEdit/src/document_view.scala Sat Mar 17 17:36:10 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sat Mar 17 17:44:29 2012 +0100
@@ -124,10 +124,10 @@
Text.Perspective(
for {
i <- 0 until text_area.getVisibleLines
- val start = text_area.getScreenLineStartOffset(i)
- val stop = text_area.getScreenLineEndOffset(i)
+ start = text_area.getScreenLineStartOffset(i)
+ stop = text_area.getScreenLineEndOffset(i)
if start >= 0 && stop >= 0
- val range <- buffer_range.try_restrict(Text.Range(start, stop))
+ range <- buffer_range.try_restrict(Text.Range(start, stop))
if !range.is_singularity
}
yield range)
@@ -388,10 +388,10 @@
if (visible_cmds.exists(changed.commands)) {
for {
line <- 0 until text_area.getVisibleLines
- val start = text_area.getScreenLineStartOffset(line) if start >= 0
- val end = text_area.getScreenLineEndOffset(line) if end >= 0
- val range = proper_line_range(start, end)
- val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+ start = text_area.getScreenLineStartOffset(line) if start >= 0
+ end = text_area.getScreenLineEndOffset(line) if end >= 0
+ range = proper_line_range(start, end)
+ line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
if line_cmds.exists(changed.commands)
} text_area.invalidateScreenLineRange(line, line)
}
--- a/src/Tools/jEdit/src/plugin.scala Sat Mar 17 17:36:10 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sat Mar 17 17:44:29 2012 +0100
@@ -181,7 +181,7 @@
def document_views(buffer: Buffer): List[Document_View] =
for {
text_area <- jedit_text_areas(buffer).toList
- val doc_view = document_view(text_area)
+ doc_view = document_view(text_area)
if doc_view.isDefined
} yield doc_view.get