# HG changeset patch
# User wenzelm
# Date 1244145997 -7200
# Node ID f37cd618f58217ba2f03950861daf53661c2e8c4
# Parent  48330c850e2fde80066d47a6ebb7ee1e694f75bd
more robust get_offsets;
set_document: removed obsolete dummy command;

diff -r 48330c850e2f -r f37cd618f582 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Jun 03 11:26:15 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Jun 04 22:06:37 2009 +0200
@@ -31,7 +31,6 @@
 {
   /* prover process */
 
-
   private val process =
   {
     val results = new EventBus[IsabelleProcess.Result] + handle_result
@@ -100,8 +99,15 @@
   private def handle_result(result: IsabelleProcess.Result)
   {
     // helper-function (move to XML?)
-    def get_attr(attributes: List[(String, String)], attr: String): Option[String] =
-      attributes.find(p => p._1 == attr).map(_._2)
+    def get_attr(attrs: List[(String, String)], name: String): Option[String] =
+      attrs.find(p => p._1 == name).map(_._2)
+
+    def get_offsets(attrs: List[(String, String)]): (Option[Int], Option[Int]) =
+    {
+      val begin = get_attr(attrs, Markup.OFFSET).map(_.toInt - 1)
+      val end = get_attr(attrs, Markup.END_OFFSET).map(_.toInt - 1)
+      (begin, if (end.isDefined) end else begin.map(_ + 1))
+    }
 
     def command_change(c: Command) = this ! c
     val (running, command) =
@@ -188,8 +194,7 @@
                     command_change(command)
                   case XML.Elem(kind, attr, body)
                   if command != null =>
-                    val begin = get_attr(attr, Markup.OFFSET).map(_.toInt - 1)
-                    val end = get_attr(attr, Markup.END_OFFSET).map(_.toInt - 1)
+                    val (begin, end) = get_offsets(attr)
                     if (begin.isDefined && end.isDefined) {
                       if (kind == Markup.ML_TYPING) {
                         val info = body.first.asInstanceOf[XML.Text].content
@@ -213,8 +218,7 @@
                   if command == null =>
                     // TODO: This is mostly irrelevant information on removed commands, but it can
                     // also be outer-syntax-markup since there is no id in props (fix that?)
-                    val begin = get_attr(attr, Markup.OFFSET).map(_.toInt - 1)
-                    val end = get_attr(attr, Markup.END_OFFSET).map(_.toInt - 1)
+                    val (begin, end) = get_offsets(attr)
                     val markup_id = get_attr(attr, Markup.ID)
                     val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
                     if (outer && !running && begin.isDefined && end.isDefined && markup_id.isDefined)
@@ -268,7 +272,6 @@
   def set_document(change_receiver: Actor, path: String) {
     this.change_receiver = change_receiver
     this ! ProverEvents.SetIsCommandKeyword(command_decls.contains)
-    process.ML("()")  // FIXME force initial writeln
     process.begin_document(document_id0, path)
   }