# HG changeset patch
# User wenzelm
# Date 1229727307 -3600
# Node ID f2644d2a3e8ec2ac5400fab8189c47171612f344
# Parent  e61e2ab1f6f751ee461e615338e19582beb73452
misc tuning;

diff -r e61e2ab1f6f7 -r f2644d2a3e8e src/Tools/jEdit/src/proofdocument/Text.scala
--- 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 {
diff -r e61e2ab1f6f7 -r f2644d2a3e8e src/Tools/jEdit/src/prover/Command.scala
--- 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 = 
diff -r e61e2ab1f6f7 -r f2644d2a3e8e src/Tools/jEdit/src/prover/Prover.scala
--- 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