--- a/src/Tools/jEdit/src/proofdocument/Text.scala Fri Dec 19 23:54:24 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala Fri Dec 19 23:55:07 2008 +0100
@@ -9,7 +9,7 @@
import isabelle.utils.EventSource
object Text {
- class Changed(val start : Int, val added : Int, val removed : Int) { }
+ class Changed(val start : Int, val added : Int, val removed : Int)
}
trait Text {
--- a/src/Tools/jEdit/src/prover/Command.scala Fri Dec 19 23:54:24 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Fri Dec 19 23:55:07 2008 +0100
@@ -60,15 +60,15 @@
var results = Nil : List[XML.Tree]
def idString = java.lang.Long.toString(id, 36)
- def results_xml = XML.document(results match {
- case Nil => XML.Elem("message", List(), List())
- case List(elem) => elem
- case _ =>
- XML.Elem("messages", List(), List(results.first,
- results.last))
- }, "style")
+ def results_xml = XML.document(
+ results match {
+ case Nil => XML.Elem("message", Nil, Nil)
+ case List(elem) => elem
+ case _ =>
+ XML.Elem("messages", List(), List(results.first, results.last))
+ }, "style")
def addResult(tree : XML.Tree) {
- results = results ::: List(tree)
+ results = results ::: List(tree) // FIXME canonical reverse order
}
val root_node =
--- a/src/Tools/jEdit/src/prover/Prover.scala Fri Dec 19 23:54:24 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Fri Dec 19 23:55:07 2008 +0100
@@ -83,7 +83,7 @@
// expecting markups here
case Elem(kind, List(("offset", offset),
("end_offset", end_offset),
- ("id", id)), List()) =>
+ ("id", id)), Nil) =>
val begin = Int.unbox(java.lang.Integer.valueOf(offset)) - 1
val end = Int.unbox(java.lang.Integer.valueOf(end_offset)) - 1