# HG changeset patch
# User immler@in.tum.de
# Date 1241014102 -7200
# Node ID 647a2430d1cdf6d401dc2fd517cbe10058c00d78
# Parent  09a5984250a21e51035a73b73006df36c7fcbe58
immutable markup-nodes;
more seperate nodes in command;
restructured handling of markups in prover

diff -r 09a5984250a2 -r 647a2430d1cd src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Apr 27 17:33:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Wed Apr 29 16:08:22 2009 +0200
@@ -53,9 +53,10 @@
     if (st == Command.Status.UNPROCESSED) {
       state_results.clear
       // delete markup
-      for (child <- root_node.children) {
-        child.children = Nil
-      }
+      state_markup = empty_root_node
+      highlight_markup = empty_root_node
+      types_markup = empty_root_node
+      refs_markup = empty_root_node
     }
     _status = st
   }
@@ -79,23 +80,24 @@
 
   /* markup */
 
-  val root_node =
-    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, content, Markup.COMMAND_SPAN)
+  val empty_root_node =
+    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil, id, content, Markup.COMMAND_SPAN)
+
+  var command_markup = empty_root_node
 
-  def add_markup(desc: String, begin: Int, end: Int) = {
-    val markup_content = if (end <= content.length) content.substring(begin, end)
-      else {
-        System.err.println (root_node.stop, content, content.length, end)
-        "wrong indices?"
-      }
-    root_node insert new MarkupNode(this, begin, end, id, markup_content, desc)
-  }
+  var state_markup = empty_root_node
+  var highlight_markup = empty_root_node
+  var types_markup = empty_root_node
+  var refs_markup = empty_root_node
+  var state_markups = List(state_markup, highlight_markup, types_markup, refs_markup)
 
-  // syntax highlighting
-  val highlight_node =
-   new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, content, Markup.COMMAND_SPAN)
+  def highlight_node = (command_markup /: highlight_markup.children) (_ + _)
+
+  def root_node = (command_markup /: state_markup.children) (_ + _)
 
-  def add_highlight(kind: String, begin: Int, end: Int) =
-    highlight_node insert new MarkupNode(this, begin, end, id, "", kind)
+  def markup_node(desc: String, begin: Int, end: Int) =
+    new MarkupNode(this, begin, end, Nil, id,
+                   if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??",
+                   desc)
 
 }
diff -r 09a5984250a2 -r 647a2430d1cd src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Mon Apr 27 17:33:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed Apr 29 16:08:22 2009 +0200
@@ -38,30 +38,24 @@
 }
 
 class MarkupNode (val base : Command, val start : Int, val stop : Int,
-                    val id : String, val content : String, val desc : String) {
+                  val children: List[MarkupNode],
+                  val id : String, val content : String, val desc : String) {
 
   def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
     val node = MarkupNode.markup2default_node (this, base, doc)
-    for (c <- children) node add c.swing_node(doc)
+    children.map(node add _.swing_node(doc))
     node
   }
-    
+
   def abs_start(doc: ProofDocument) = base.start(doc) + start
   def abs_stop(doc: ProofDocument) = base.start(doc) + stop
 
-  var parent : MarkupNode = null
-  def orphan = parent == null
-
-  var children : List[MarkupNode] = Nil
+  def set_children(newchildren: List[MarkupNode]): MarkupNode =
+    new MarkupNode(base, start, stop, newchildren, id, content, desc)
 
-  private def add(child : MarkupNode) {
-    child parent = this
-    children = (child :: children) sort ((a, b) => a.start < b.start)
-  }
+  def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start))
 
-  private def remove(nodes : List[MarkupNode]) {
-    children = children diff nodes
-  }
+  def remove(nodes : List[MarkupNode]) = set_children(children diff nodes)
 
   def dfs : List[MarkupNode] = {
     var all = Nil : List[MarkupNode]
@@ -83,42 +77,33 @@
       val filled_gaps = for {
         child <- children
         markups = if (next_x < child.start) {
-          new MarkupNode(base, next_x, child.start, id, content, "") :: child.flatten
+          new MarkupNode(base, next_x, child.start, Nil, id, content, "") :: child.flatten
         } else child.flatten
         update = (next_x = child.stop)
         markup <- markups
       } yield markup
-      if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, content, "")
+      if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, "")
       else filled_gaps
     }
   }
 
-  def insert(new_child : MarkupNode) : Unit = {
+  def +(new_child : MarkupNode) : MarkupNode = {
     if (new_child fitting_into this) {
-      for (child <- children) {
-        if (new_child fitting_into child)
-          child insert new_child
+      val new_children = children.map(c => if((new_child fitting_into c)) c + new_child else c)
+      if (new_children == children) {
+        // new_child did not fit into children of this -> insert new_child between this and its children
+        val (fitting, nonfitting) = children span(_ fitting_into new_child)
+        this remove fitting add ((new_child /: fitting) (_ add _))
       }
-      if (new_child orphan) {
-        // new_child did not fit into children of this
-        // -> insert new_child between this and its children
-        for (child <- children) {
-          if (child fitting_into new_child) {
-            new_child add child
-          }
-        }
-        this add new_child
-        this remove new_child.children
-      }
+      else this set_children new_children
     } else {
-      System.err.println("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc
+      error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc
                          + "(" +new_child.start + ", "+ new_child.stop + ")")
     }
   }
 
   // does this fit into node?
-  def fitting_into(node : MarkupNode) = node.start <= this.start &&
-    node.stop >= this.stop
+  def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop
 
   override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + desc
 }
diff -r 09a5984250a2 -r 647a2430d1cd src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Apr 27 17:33:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Apr 29 16:08:22 2009 +0200
@@ -180,37 +180,29 @@
                     output_info.event(result.toString)
                     command.status = Command.Status.FAILED
                     command_change(command)
-                  // ML typing
-                  case XML.Elem(Markup.ML_TYPING, attr, body) =>
-                    val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
-                    val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
-                    val markup_id = get_attr(attr, Markup.ID).get
-                    val info = body.first.asInstanceOf[XML.Text].content
-                    command.add_markup(info, begin, end)
-                    command_change(command)
-                  // ML references
-                  case XML.Elem(Markup.ML_REF, attr, body) =>
+                  case XML.Elem(kind, attr, body) =>
+                    // TODO: assuming that begin, end, id are present in attributes
                     val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
                     val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
                     val markup_id = get_attr(attr, Markup.ID).get
-                    command.add_markup(body.toString, begin, end)
+                    kind match {
+                      case Markup.ML_TYPING =>
+                        val info = body.first.asInstanceOf[XML.Text].content
+                        command.types_markup += command.markup_node(info, begin, end)
+                        command.state_markup += command.markup_node(info, begin, end)
+                      case Markup.ML_REF =>
+                        command.refs_markup += command.markup_node(body.toString, begin, end)
+                        command.state_markup += command.markup_node(body.toString, begin, end)
+                      case kind =>
+                        if (!running)
+                          commands.get(markup_id).map (cmd =>
+                          cmd.command_markup += cmd.markup_node(kind, begin, end))
+                        else {
+                          command.highlight_markup += command.markup_node(kind, begin, end)
+                          command.state_markup += command.markup_node(kind, begin, end)
+                        }
+                    }
                     command_change(command)
-                  // syntax highlighting
-                  case XML.Elem(kind, attr, body) =>
-                    val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
-                    val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
-                    val markup_id = get_attr(attr, Markup.ID).get
-
-                    val cmd =  // FIXME proper command version!? running!?
-                      // outer syntax: no id in props
-                      if (command == null) commands.getOrElse(markup_id, null)
-                      // inner syntax: id from props
-                      else command
-                    if (cmd != null) {
-                      cmd.add_markup(kind, begin, end)
-                      cmd.add_highlight(kind, begin, end)
-                      command_change(cmd)
-                    }
                   case _ =>
                   //}}}
                 }