merged; resolved superficial conflicts
authorimmler@in.tum.de
Tue, 02 Jun 2009 22:55:13 +0200
changeset 34597 a0c84b0edb9a
parent 34587 72b02f9c509c (current diff)
parent 34596 2b46d92e4642 (diff)
child 34598 4f2d122c0a67
merged; resolved superficial conflicts
src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
src/Tools/jEdit/src/jedit/ProverSetup.scala
src/Tools/jEdit/src/jedit/TheoryView.scala
src/Tools/jEdit/src/proofdocument/ProofDocument.scala
src/Tools/jEdit/src/proofdocument/Token.scala
src/Tools/jEdit/src/prover/Command.scala
src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Tue Jun 02 22:55:13 2009 +0200
@@ -84,24 +84,26 @@
     def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(document.id, _)
 
     var next_x = start
-    for {
-      command <- document.commands.
-        dropWhile(_.stop(document) <= from(start)).
-        takeWhile(_.start(document) < from(stop))
-      markup <- command.highlight_node.flatten
-      if (to(markup.abs_stop(document)) > start)
-      if (to(markup.abs_start(document)) < stop)
-      byte = DynamicTokenMarker.choose_byte(markup.info.toString)
-      token_start = to(markup.abs_start(document)) - start max 0
-      token_length =
-        to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
-          (start - to(markup.abs_start(document)) max 0) -
-          (to(markup.abs_stop(document)) - stop max 0)
-    } {
-      if (start + token_start > next_x)
-        handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
-      handler.handleToken(line_segment, byte, token_start, token_length, context)
-      next_x = start + token_start + token_length
+
+    var command = document.find_command_at(from(start))
+    while (command != null && command.start(document) < from(stop)) {
+      for {
+        markup <- command.highlight_node.flatten
+        if (to(markup.abs_stop(document)) > start)
+        if (to(markup.abs_start(document)) < stop)
+        byte = DynamicTokenMarker.choose_byte(markup.info.toString)
+        token_start = to(markup.abs_start(document)) - start max 0
+        token_length =
+          to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
+            (start - to(markup.abs_start(document)) max 0) -
+            (to(markup.abs_stop(document)) - stop max 0)
+      } {
+        if (start + token_start > next_x)
+          handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)
+        handler.handleToken(line_segment, byte, token_start, token_length, context)
+        next_x = start + token_start + token_length
+      }
+      command = document.commands.next(command).getOrElse(null)
     }
     if (next_x < stop)
       handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Jun 02 22:55:13 2009 +0200
@@ -43,8 +43,11 @@
       if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length)
       else path)
     theory_view.activate
-    prover ! new isabelle.proofdocument.Text.Change(
-      Isabelle.plugin.id(), 0, buffer.getText(0, buffer.getLength), 0)
+    val MCL = TheoryView.MAX_CHANGE_LENGTH
+    for (i <- 0 to buffer.getLength / MCL)
+      prover ! new isabelle.proofdocument.Text.Change(
+        Isabelle.plugin.id(), i * MCL,
+        buffer.getText(i * MCL, MCL min buffer.getLength - i * MCL),0)
 
     //register output-view
     prover.output_info += (text =>
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Jun 02 22:55:13 2009 +0200
@@ -195,14 +195,14 @@
     val saved_color = gfx.getColor
 
     val metrics = text_area.getPainter.getFontMetrics
+
+    // encolor phase
     var e = document.find_command_at(from_current(start))
-    val commands = document.commands.dropWhile(_.stop(document) <= from_current(start)).
-      takeWhile(c => to_current(c.start(document)) < end)
-    // encolor phase
-    for (e <- commands) {
+    while (e != null && e.start(document) < end) {
       val begin = start max to_current(e.start(document))
       val finish = end - 1 min to_current(e.stop(document))
       encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
+      e = document.commands.next(e).getOrElse(null)
     }
 
     gfx.setColor(saved_color)
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jun 02 22:55:13 2009 +0200
@@ -61,7 +61,7 @@
     return (doc.mark_active, change)
   }
   def set_command_keyword(f: String => Boolean): ProofDocument =
-    new ProofDocument(id, tokens, token_start, commands, active, f)
+    new ProofDocument(isabelle.jedit.Isabelle.plugin.id(), tokens, token_start, commands, active, f)
 
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
   /** token view **/
@@ -126,7 +126,8 @@
         case t :: ts =>
           if (start(t) == start(new_token) &&
               start(t) > change.start + change.added.length) {
-          old_suffix = ts
+          old_suffix = t :: ts
+          new_tokens = new_tokens.tail
           invalid_tokens = Nil
         }
         case _ =>
@@ -134,42 +135,45 @@
     }
     val insert = new_tokens.reverse
     val new_token_list = begin ::: insert ::: old_suffix
-    val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
     token_changed(change.id, begin.lastOption, insert,
-      old_suffix.firstOption, new_tokenset, start)
+      old_suffix.firstOption, new_token_list, start)
   }
 
   
   /** command view **/
 
-  def find_command_at(pos: Int): Command = {
-    for (cmd <- commands) { if (pos < cmd.stop(this)) return cmd }
-    return null
-  }
-
   private def token_changed(
     new_id: String,
     before_change: Option[Token],
     inserted_tokens: List[Token],
     after_change: Option[Token],
-    new_tokenset: LinearSet[Token],
+    new_tokens: List[Token],
     new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) =
   {
-    val cmd_first_changed =
-      if (before_change.isDefined) commands.find(_.tokens.contains(before_change.get))
-      else None
-    val cmd_last_changed =
-      if (after_change.isDefined) commands.find(_.tokens.contains(after_change.get))
-      else None
+    val new_tokenset = (LinearSet() ++ new_tokens).asInstanceOf[LinearSet[Token]]
+    val cmd_before_change = before_change match {
+      case None => None
+      case Some(bc) =>
+        val cmd_with_bc = commands.find(_.contains(bc)).get
+        if (cmd_with_bc.tokens.last == bc) {
+          if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
+            Some(cmd_with_bc)
+          else commands.prev(cmd_with_bc)
+        }
+        else commands.prev(cmd_with_bc)
+    }
 
-    val cmd_before_change =
-      if (cmd_first_changed.isDefined) commands.prev(cmd_first_changed.get)
-      else None
-    val cmd_after_change =
-      if (cmd_last_changed.isDefined) commands.next(cmd_last_changed.get)
-      else None
+    val cmd_after_change = after_change match {
+      case None => None
+      case Some(ac) =>
+        val cmd_with_ac = commands.find(_.contains(ac)).get
+        if (ac.is_start)
+          Some(cmd_with_ac)
+        else
+          commands.next(cmd_with_ac)
+    }
 
-    val removed_commands = commands.dropWhile(Some(_) != cmd_first_changed).
+    val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
       takeWhile(Some(_) != cmd_after_change)
 
     // calculate inserted commands
@@ -183,21 +187,33 @@
       }
     }
 
-    val split_begin_tokens =
-      if (!cmd_first_changed.isDefined || !before_change.isDefined) Nil
-      else {
-        cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) :::
-          List(before_change.get)
-      }
-    val split_end_tokens =
-      if (!cmd_last_changed.isDefined || !after_change.isDefined) Nil
-      else {
-        cmd_last_changed.get.tokens.dropWhile(_ != after_change.get)
-      }
+    val split_begin =
+      if (before_change.isDefined) {
+        val changed =
+          if (cmd_before_change.isDefined)
+            new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
+          else new_tokenset
+        if (changed.exists(_ == before_change.get))
+          changed.takeWhile(_ != before_change.get).toList :::
+            List(before_change.get)
+        else Nil
+      } else Nil
 
+    val split_end =
+      if (after_change.isDefined && cmd_after_change.isDefined) {
+        val unchanged = new_tokens.dropWhile(_ != after_change.get)
+        if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
+          unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
+        else Nil
+      } else Nil
+
+    val rescan_begin =
+      split_begin :::
+        before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
     val rescanning_tokens =
-      split_begin_tokens ::: inserted_tokens ::: split_end_tokens
-    val inserted_commands = tokens_to_commands(rescanning_tokens)
+      after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
+        split_end
+    val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
 
     val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList)
     // build new document
@@ -209,4 +225,30 @@
         new_commandset, active, is_command_keyword)
     return (doc, change)
   }
+
+  val commands_offsets = {
+    var last_stop = 0
+    (for (c <- commands) yield {
+      val r = c -> (last_stop,c.stop(this))
+      last_stop = c.stop(this)
+      r
+    }).toArray
+  }
+
+  // use a binary search to find commands for a given offset
+  def find_command_at(pos: Int): Command = find_command_at(pos, 0, commands_offsets.length)
+  private def find_command_at(pos: Int, array_start: Int, array_stop: Int): Command = {
+    val middle_index = (array_start + array_stop) / 2
+    if (middle_index >= commands_offsets.length) return null
+    val (middle, (start, stop)) = commands_offsets(middle_index)
+    // does middle contain pos?
+    if (start <= pos && stop > pos)
+      middle
+    else if (start > pos)
+      find_command_at(pos, array_start, middle_index)
+    else if (stop <= pos)
+      find_command_at(pos, middle_index + 1, array_stop)
+    else error("can't be")
+  }
+
 }
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jun 02 22:55:13 2009 +0200
@@ -32,6 +32,8 @@
 }
 
 class Token(val content: String, val kind: Token.Kind.Value) {
+  import Token.Kind._
   val length = content.length
   override def toString = content
+  val is_start = kind == COMMAND_START || kind == COMMENT
 }
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jun 02 22:55:13 2009 +0200
@@ -43,6 +43,8 @@
   def start(doc: ProofDocument) = doc.token_start(tokens.first)
   def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
 
+  def contains(p: Token) = tokens.contains(p)
+
   /* command status */
 
   var state_id: IsarDocument.State_ID = null
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Tue Jun 02 22:00:28 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Tue Jun 02 22:55:13 2009 +0200
@@ -125,8 +125,8 @@
       }
       else this set_children new_children
     } else {
-      error("ignored nonfitting markup " + new_child.id + new_child.content +
-        new_child.info.toString + "(" +new_child.start + ", "+ new_child.stop + ")")
+      System.err.println("ignored nonfitting markup: " + new_child)
+      this
     }
   }