# HG changeset patch
# User immler@in.tum.de
# Date 1235072668 -3600
# Node ID b504abb6eff6b2fbf0a32c52aaa169b143735800
# Parent  452a588f795491b9dad7edcd08f45a81518ae094
tokens and commands as lists

diff -r 452a588f7954 -r b504abb6eff6 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Thu Feb 19 20:44:28 2009 +0100
@@ -32,10 +32,9 @@
     val prover_setup = Isabelle.plugin.prover_setup(buffer)
     if (prover_setup.isDefined) {
         val document = prover_setup.get.prover.document
-        val commands = document.commands
-        while (!stopped && commands.hasNext) {
-          data.root.add(commands.next.root_node.swing_node)
-        }
+        for (command <- document.commands)
+          data.root.add(command.root_node.swing_node)
+        
         if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
     } else {
       data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
@@ -51,7 +50,7 @@
   override def canCompleteAnywhere = true
   override def getInstantCompletionTriggers = "\\"
 
-  override def complete(pane: EditPane, caret: Int): SideKickCompletion = {
+  override def complete(pane: EditPane, caret: Int): SideKickCompletion = null /*{
     val buffer = pane.getBuffer
     val ps = Isabelle.prover_setup(buffer)
     if (ps.isDefined) {
@@ -83,7 +82,7 @@
       }
       return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
     } else return null
-  }
+  }*/
 
 }
 
diff -r 452a588f7954 -r b504abb6eff6 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Feb 19 20:44:28 2009 +0100
@@ -46,7 +46,7 @@
   buffer.addBufferListener(this)
 
 
-  private var col: Text.Changed = null
+  private var col: Text.Change = null
 
   private val col_timer = new Timer(300, new ActionListener() {
     override def actionPerformed(e: ActionEvent) = commit
@@ -88,6 +88,7 @@
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
     buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover.document))
     update_styles
+    changes.event(new Text.Change(0,buffer.getText(0, buffer.getLength),0))
   }
 
   def deactivate() = {
@@ -104,14 +105,14 @@
 
   def from_current (pos: Int) =
     if (col != null && col.start <= pos)
-      if (pos < col.start + col.added) col.start
-      else pos - col.added + col.removed
+      if (pos < col.start + col.added.length) col.start
+      else pos - col.added.length + col.removed
     else pos
 
   def to_current (pos : Int) =
     if (col != null && col.start <= pos)
       if (pos < col.start + col.removed) col.start
-      else pos + col.added - col.removed
+      else pos + col.added.length - col.removed
     else pos
 
   def repaint(cmd: Command) =
@@ -162,9 +163,10 @@
 
     val metrics = text_area.getPainter.getFontMetrics
     var e = prover.document.find_command_at(from_current(start))
-
+    val commands = prover.document.commands.dropWhile(_.stop <= from_current(start)).
+      takeWhile(c => to_current(c.start) < end)
     // encolor phase
-    while (e != null && to_current(e.start) < end) {
+    for (e <- commands) {
       val begin = start max to_current(e.start)
       val finish = end - 1 min to_current(e.stop)
       encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
@@ -178,7 +180,6 @@
             DynamicTokenMarker.choose_color(node.kind), true)
         }
       }
-      e = e.next
     }
 
     gfx.setColor(saved_color)
@@ -189,7 +190,7 @@
 
   def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
   def length = buffer.getLength
-  val changes = new EventBus[Text.Changed]
+  val changes = new EventBus[Text.Change]
 
 
   /* BufferListener methods */
@@ -219,13 +220,14 @@
   override def preContentInserted(buffer: JEditBuffer,
     start_line: Int, offset: Int, num_lines: Int, length: Int) =
   {
+    val text = buffer.getText(offset, length)
     if (col == null)
-      col = new Text.Changed(offset, length, 0)
-    else if (col.start <= offset && offset <= col.start + col.added)
-      col = new Text.Changed(col.start, col.added + length, col.removed)
+      col = new Text.Change(offset, text, 0)
+    else if (col.start <= offset && offset <= col.start + col.added.length)
+      col = new Text.Change(col.start, col.added + text, col.removed)
     else {
       commit
-      col = new Text.Changed(offset, length, 0)
+      col = new Text.Change(offset, text, 0)
     }
     delay_commit
   }
@@ -234,20 +236,22 @@
     start_line: Int, start: Int, num_lines: Int, removed: Int) =
   {
     if (col == null)
-      col = new Text.Changed(start, 0, removed)
-    else if (col.start > start + removed || start > col.start + col.added) {
+      col = new Text.Change(start, "", removed)
+    else if (col.start > start + removed || start > col.start + col.added.length) {
       commit
-      col = new Text.Changed(start, 0, removed)
+      col = new Text.Change(start, "", removed)
     }
     else {
-      val offset = start - col.start
-      val diff = col.added - removed
+/*      val offset = start - col.start
+      val diff = col.added.length - removed
       val (added, add_removed) =
         if (diff < offset)
           (offset max 0, diff - (offset max 0))
         else
           (diff - (offset min 0), offset min 0)
-      col = new Text.Changed(start min col.start, added, col.removed - add_removed)
+      col = new Text.Changed(start min col.start, added, col.removed - add_removed)*/
+      commit
+      col = new Text.Change(start, "", removed)
     }
     delay_commit
   }
diff -r 452a588f7954 -r b504abb6eff6 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Feb 19 20:44:28 2009 +0100
@@ -7,13 +7,13 @@
 
 package isabelle.proofdocument
 
-
+import scala.collection.mutable.ListBuffer
 import java.util.regex.Pattern
 import isabelle.prover.{Prover, Command}
 
 
 case class StructureChange(
-  val before_change: Command,
+  val before_change: Option[Command],
   val added_commands: List[Command],
   val removed_commands: List[Command])
 
@@ -39,69 +39,45 @@
 
 class ProofDocument(text: Text, is_command_keyword: String => Boolean)
 {
-  private var active = false 
+  private var active = false
   def activate() {
     if (!active) {
       active = true
-      text_changed(0, text.length, 0)
+      text_changed(new Text.Change(0, content, content.length))
     }
   }
 
-  text.changes += (changed => text_changed(changed.start, changed.added, changed.removed))
+  text.changes += (change => text_changed(change))
 
-
-
+  var tokens = Nil : List[Token]
+  var commands = Nil : List[Command]
+  def content = Token.string_from_tokens(tokens)
   /** token view **/
 
-  private var first_token: Token = null
-  private var last_token: Token = null
-  
-  private def tokens(start: Token, stop: Token) = new Iterator[Token] {
-      var current = start
-      def hasNext = current != stop && current != null
-      def next() = { val save = current; current = current.next; save }
-    }
-  private def tokens(start: Token): Iterator[Token] = tokens(start, null)
-  private def tokens(): Iterator[Token] = tokens(first_token, null)
-
-
-  private def text_changed(start: Int, added_len: Int, removed_len: Int)
+  private def text_changed(change: Text.Change)
   {
-    if (!active)
-      return
+    val (begin, remaining) = tokens.span(_.stop < change.start)
+    val (removed, end) = remaining.span(_.start <= change.start + change.removed)
+    for (t <- end) t.start += (change.added.length - change.removed)
 
-    var before_change =
-      if (Token.check_stop(first_token, _ < start)) Token.scan(first_token, _.stop >= start)
-      else null
-    
-    var first_removed =
-      if (before_change != null) before_change.next
-      else if (Token.check_start(first_token, _ <= start + removed_len)) first_token
-      else null 
-
-    var last_removed = Token.scan(first_removed, _.start > start + removed_len)
+    val split_begin = removed.takeWhile(_.start < change.start).
+      map (t => new Token(t.start,
+                          t.content.substring(0, change.start - t.start),
+                          t.kind))
+    val split_end = removed.dropWhile(_.stop < change.start + change.removed).
+      map (t => new Token(change.start + change.added.length,
+                          t.content.substring(change.start + change.removed - t.start),
+                          t.kind))
 
-    var shift_token =
-      if (last_removed != null) last_removed
-      else if (Token.check_start(first_token, _ > start)) first_token
-      else null
-    
-    while (shift_token != null) {
-      shift_token.shift(added_len - removed_len, start)
-      shift_token = shift_token.next
-    }
-    
-    // scan changed tokens until the end of the text or a matching token is
-    // found which is beyond the changed area
-    val match_start = if (before_change == null) 0 else before_change.stop
-    var first_added: Token = null
-    var last_added: Token = null
+    var invalid_tokens =  split_begin :::
+      new Token(change.start, change.added, Token.Kind.OTHER) :: split_end ::: end
+    var new_tokens = Nil: List[Token]
+    var old_suffix = Nil: List[Token]
 
-    val matcher = ProofDocument.token_pattern.matcher(text.content(match_start, text.length))
-    var finished = false
-    var position = 0 
-    while (matcher.find(position) && !finished) {
-      position = matcher.end
+    val match_start = invalid_tokens.first.start
+    val matcher = ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens))
+
+    while (matcher.find() && invalid_tokens != Nil) {
 			val kind =
         if (is_command_keyword(matcher.group))
           Token.Kind.COMMAND_START
@@ -109,251 +85,89 @@
           Token.Kind.COMMENT
         else
           Token.Kind.OTHER
-      val new_token = new Token(matcher.start + match_start, matcher.end + match_start, kind)
-
-      if (first_added == null)
-        first_added = new_token
-      else {
-        new_token.prev = last_added
-        last_added.next = new_token
-      }
-      last_added = new_token
-      
-      while (Token.check_stop(last_removed, _ < new_token.stop) &&
-              last_removed.next != null)
-        last_removed = last_removed.next
-			
-      if (new_token.stop >= start + added_len &&
-            Token.check_stop(last_removed, _ == new_token.stop))
-        finished = true
-    }
+      val new_token = new Token(match_start + matcher.start, matcher.group, kind)
+      new_tokens ::= new_token
 
-    var after_change = if (last_removed != null) last_removed.next else null
-		
-    // remove superflous first token-change
-    if (first_added != null && first_added == first_removed &&
-          first_added.stop < start) {
-      before_change = first_removed
-      if (last_removed == first_removed) {
-        last_removed = null
-        first_removed = null
-      }
-      else {
-        first_removed = first_removed.next
-        assert(first_removed != null)
-      }
-
-      if (last_added == first_added) {
-        last_added = null
-        first_added = null
-      }
-      if (first_added != null)
-        first_added = first_added.next
-    }
-    
-    // remove superflous last token-change
-    if (last_added != null && last_added == last_removed &&
-          last_added.start > start + added_len) {
-      after_change = last_removed
-      if (first_removed == last_removed) {
-        first_removed = null
-        last_removed = null
-      }
-      else {
-        last_removed = last_removed.prev
-        assert(last_removed != null)
+      invalid_tokens = invalid_tokens dropWhile (_.stop < new_token.stop)
+      invalid_tokens match {
+        case t::ts => if(t.start == new_token.start &&
+                         t.start > change.start + change.added.length) {
+          old_suffix = ts
+          invalid_tokens = Nil
+        }
+        case _ =>
       }
-      
-      if (last_added == first_added) {
-        last_added = null
-        first_added = null
-      }
-      else
-        last_added = last_added.prev
     }
-    
-    if (first_removed == null && first_added == null)
-      return
-    
-    if (first_token == null) {
-      first_token = first_added
-      last_token = last_added
-    }
-    else {
-      // cut removed tokens out of list
-      if (first_removed != null)
-        first_removed.prev = null
-      if (last_removed != null)
-        last_removed.next = null
-      
-      if (first_token == first_removed)
-        if (first_added != null)
-          first_token = first_added
-        else
-          first_token = after_change
-      
-      if (last_token == last_removed)
-        if (last_added != null)
-          last_token = last_added
-        else
-          last_token = before_change
-      
-      // insert new tokens into list
-      if (first_added != null) {
-        first_added.prev = before_change
-        if (before_change != null)
-          before_change.next = first_added
-        else
-          first_token = first_added
-      }
-      else if (before_change != null)
-        before_change.next = after_change
-      
-      if (last_added != null) {
-        last_added.next = after_change
-        if (after_change != null)
-          after_change.prev = last_added
-        else
-          last_token = last_added
-      }
-      else if (after_change != null)
-        after_change.prev = before_change
-    }
-    
-    token_changed(before_change, after_change, first_removed)
+    val insert = new_tokens.reverse
+    tokens = begin ::: insert ::: old_suffix
+
+    token_changed(begin.lastOption,
+                  insert,
+                  removed,
+                  old_suffix.firstOption)
   }
   
-
-  
   /** command view **/
 
   val structural_changes = new EventBus[StructureChange]
 
-  def commands_from(start: Token) = new Iterator[Command] {
-    var current = start
-    def hasNext = current != null
-    def next = { val s = current.command ; current = s.last.next ; s }
-  }
-  def commands_from(start: Command): Iterator[Command] = commands_from(start.first)
-  def commands = commands_from(first_token)
-
   def find_command_at(pos: Int): Command = {
     for (cmd <- commands) { if (pos < cmd.stop) return cmd }
     return null
   }
 
-  private def token_changed(start: Token, stop: Token, removed: Token)
+  private def token_changed(before_change: Option[Token],
+                            inserted_tokens: List[Token],
+                            removed_tokens: List[Token],
+                            after_change: Option[Token])
   {
-    var removed_commands: List[Command] = Nil
-    var first: Command = null
-    var last: Command = null
-
-    for (t <- tokens(removed)) {
-      if (first == null)
-        first = t.command
-      if (t.command != last)
-        removed_commands = t.command :: removed_commands
-      last = t.command
+    val (begin, remaining) =
+      before_change match {
+        case None => (Nil, commands)
+        case Some(bc) => commands.break(_.tokens.contains(bc))
+      }
+    val (_removed, _end) =
+      after_change match {
+        case None => (remaining, Nil)
+        case Some(ac) => remaining.break(_.tokens.contains(ac))
+      }
+    val (removed, end) = _end match {
+      case Nil => (_removed, Nil)
+      case acc::end => if (after_change.isDefined && after_change.get.kind == Token.Kind.COMMAND_START)
+          (_removed, _end)
+        else (_removed ::: List(acc), end)
     }
-
-    var before: Command = null
-    if (!removed_commands.isEmpty) {
-      if (first.first == removed) {
-        if (start == null)
-          before = null
-        else
-          before = start.command
+    val all_removed_tokens = for(c <- removed; t <- c.tokens) yield t
+    val (pseudo_new_pre, rest) =
+      if (! before_change.isDefined) (Nil, all_removed_tokens)
+      else {
+        val (a, b) = all_removed_tokens.span (_ != before_change.get)
+        b match {
+          case Nil => (a, Nil)
+          case bc::rest => (a ::: List(bc), b)
+        }
       }
-      else
-        before = first.prev
-    }
+    val pseudo_new_post = rest.dropWhile(Some(_) != after_change)
 
-    var added_commands: List[Command] = Nil
-    var scan: Token = null
-    if (start != null) {
-      val next = start.next
-      if (first != null && first.first != removed) {
-        scan = first.first
-        if (before == null)
-          before = first.prev
-      }
-      else if (next != null && next != stop) {
-        if (next.kind == Token.Kind.COMMAND_START) {
-          before = start.command
-          scan = next
-        }
-        else if (first == null || first.first == removed) {
-          first = start.command
-          removed_commands = first :: removed_commands
-          scan = first.first
-          if (before == null)
-            before = first.prev
-        }
-        else {
-          scan = first.first
-          if (before == null)
-            before = first.prev
-        }
+    def tokens_to_commands(tokens: List[Token]): List[Command]= {
+      tokens match {
+        case Nil => Nil
+        case t::ts =>
+          val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
+          new Command(t::cmd) :: tokens_to_commands (rest)
       }
     }
-    else
-      scan = first_token
 
-    var stop_scan: Token = null
-    if (stop != null) {
-      if (stop == stop.command.first)
-        stop_scan = stop
-      else
-        stop_scan = stop.command.last.next
-    }
-    else if (last != null)
-      stop_scan = last.last.next
-    else
-      stop_scan = null
-
-    var cmd_start: Token = null
-    var cmd_stop: Token = null
-    var overrun = false
-    var finished = false
-    while (scan != null && !finished) {
-      if (scan == stop_scan) {
-        if (scan.kind == Token.Kind.COMMAND_START)
-          finished = true
-        else
-          overrun = true
-      }
+    System.err.println("ins_tokens: " + inserted_tokens)
+    val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
+    System.err.println("new_commands: " + new_commands)
 
-      if (scan.kind == Token.Kind.COMMAND_START && cmd_start != null && !finished) {
-        if (!overrun) {
-          added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
-          cmd_start = scan
-          cmd_stop = scan
-        }
-        else
-          finished = true
-      }
-      else if (!finished) {
-        if (cmd_start == null)
-          cmd_start = scan
-        cmd_stop = scan
-      }
-      if (overrun && !finished) {
-        if (scan.command != last)
-          removed_commands = scan.command :: removed_commands
-        last = scan.command
-      }
-
-      if (!finished)
-        scan = scan.next
-    }
-
-    if (cmd_start != null)
-      added_commands = new Command(text, cmd_start, cmd_stop) :: added_commands
-
-    // relink commands
-    added_commands = added_commands.reverse
-    removed_commands = removed_commands.reverse
-
-    structural_changes.event(new StructureChange(before, added_commands, removed_commands))
+    commands = begin ::: new_commands ::: end
+    val before = begin match {case Nil => None case _ => Some (begin.last)}
+    structural_changes.event(new StructureChange(before, new_commands, removed))
+/*
+    val old = commands
+    commands = tokens_to_commands(tokens)
+    structural_changes.event(new StructureChange(None, commands, old)) */
   }
 }
diff -r 452a588f7954 -r b504abb6eff6 src/Tools/jEdit/src/proofdocument/Text.scala
--- a/src/Tools/jEdit/src/proofdocument/Text.scala	Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Text.scala	Thu Feb 19 20:44:28 2009 +0100
@@ -8,11 +8,11 @@
 
 
 object Text {
-  case class Changed(val start: Int, val added: Int, val removed: Int)
+  case class Change(start: Int, val added: String, val removed: Int) {
+    override def toString = "start: " + start + " added: " + added + " removed: " + removed
+  }
 }
 
 trait Text {
-  def content(start: Int, stop: Int): String
-  def length: Int
-  def changes: EventBus[Text.Changed]
+  def changes: EventBus[Text.Change]
 }
diff -r 452a588f7954 -r b504abb6eff6 src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Thu Feb 19 20:44:28 2009 +0100
@@ -18,43 +18,28 @@
     val OTHER = Value("OTHER")
   }
 
-  def check_start(t: Token, P: Int => Boolean) = { t != null && P(t.start) }
-  def check_stop(t: Token, P: Int => Boolean) = { t != null && P(t.stop) }
+  def check_start(t: Token, P: Int => Boolean) = t != null && P(t.start)
+  def check_stop(t: Token, P: Int => Boolean) = t != null && P(t.stop)
 
-  def scan(s: Token, f: Token => Boolean): Token =
-  {
-    var current = s
-    while (current != null) {
-      val next = current.next
-      if (next == null || f(next)) return current
-      current = next
+  private def fill(n: Int) = {
+    val blanks = new Array[Char](n)
+    for(i <- 0 to n - 1) blanks(i) = ' '
+    new String(blanks)
+  }
+  def string_from_tokens (tokens: List[Token]): String = {
+    tokens match {
+      case Nil => ""
+      case t::tokens => (tokens.foldLeft
+          (t.content, t.stop)
+          ((a, token) => (a._1 + fill(token.start - a._2) + token.content, token.stop))
+        )._1
     }
-    return null
   }
+
 }
 
-class Token(var start: Int, var stop: Int, val kind: Token.Kind.Value)
-{
-  var next: Token = null
-  var prev: Token = null
-  var command: Command = null
-  
-  def length = stop - start
-
-  def shift(offset: Int, bottom_clamp: Int) {
-    start = bottom_clamp max (start + offset)
-    stop = bottom_clamp max (stop + offset)
-  }
-  
-  override def hashCode: Int = (31 + start) * 31 + stop
-
-  override def equals(obj: Any): Boolean =
-  {
-    if (super.equals(obj)) return true
-    if (null == obj) return false
-    obj match {
-      case other: Token => (start == other.start) && (stop == other.stop)
-      case other: Any => false
-    }
-  }
+class Token(var start: Int, val content: String, val kind: Token.Kind.Value) {
+  val length = content.length
+  def stop = start + length
+  override def toString = content + "(" + kind + ")"
 }
diff -r 452a588f7954 -r b504abb6eff6 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Thu Feb 19 20:44:28 2009 +0100
@@ -29,40 +29,19 @@
 }
 
 
-class Command(text: Text, val first: Token, val last: Token)
+class Command(val tokens: List[Token])
 {
   val id = Isabelle.plugin.id()
 
-
   /* content */
 
-  {
-    var t = first
-    while (t != null) {
-      t.command = this
-      t = if (t == last) null else t.next
-    }
-  }
-
   override def toString = name
 
-  val name = text.content(first.start, first.stop)
-  val content = text.content(proper_start, proper_stop)
-
-  def next = if (last.next != null) last.next.command else null
-  def prev = if (first.prev != null) first.prev.command else null
-
-  def start = first.start
-  def stop = last.stop
+  val name = tokens.head.content
+  val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT))
 
-  def proper_start = start
-  def proper_stop = {
-    var i = last
-    while (i != first && i.kind == Token.Kind.COMMENT)
-      i = i.prev
-    i.stop
-  }
-
+  def start = tokens.first.start
+  def stop = tokens.last.stop
 
   /* command status */
 
diff -r 452a588f7954 -r b504abb6eff6 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Feb 05 21:18:30 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Feb 19 20:44:28 2009 +0100
@@ -195,23 +195,19 @@
     this.document = new ProofDocument(text, command_decls.contains(_))
     process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
 
-    document.structural_changes += (changes => {
+    document.structural_changes += (changes => if(initialized){
       for (cmd <- changes.removed_commands) remove(cmd)
-      for (cmd <- changes.added_commands) send(cmd)
+      changes.added_commands.foldLeft (changes.before_change) ((p, c) => {send(p, c); Some(c)})
     })
-    if (initialized) {
-      document.activate()
-      activated.event(())
-    }
   }
 
-  private def send(cmd: Command) {
+  private def send(prev: Option[Command], cmd: Command) {
     cmd.status = Command.Status.UNPROCESSED
     commands.put(cmd.id, cmd)
 
     val content = isabelle_system.symbols.encode(cmd.content)
     process.create_command(cmd.id, content)
-    process.insert_command(if (cmd.prev == null) "" else cmd.prev.id, cmd.id)
+    process.insert_command(prev match {case Some(c) => c.id case None => ""}, cmd.id)
   }
 
   def remove(cmd: Command) {