--- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 21:20:22 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Jun 02 21:27:51 2009 +0200
@@ -106,7 +106,7 @@
}
}
}
- }.start
+ }
def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int =
changes match {