# HG changeset patch
# User wenzelm
# Date 1252104239 -7200
# Node ID 611864f2729db32800491e9947d8bcba861e1781
# Parent  cc5d388fcbf26274311f36f63ff8f59deb035de3
tuned MarkupNode argument order;
tuned;

diff -r cc5d388fcbf2 -r 611864f2729d src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Sat Sep 05 00:35:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sat Sep 05 00:43:59 2009 +0200
@@ -87,13 +87,13 @@
 
   lazy val empty_root_node =
     new MarkupNode(0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
-      Nil, content, Command.RootInfo)
+      content, Command.RootInfo, Nil)
 
   def markup_node(begin: Int, end: Int, info: Any): MarkupNode =
   {
     val start = symbol_index.decode(begin)
     val stop = symbol_index.decode(end)
-    new MarkupNode(start, stop, Nil, content.substring(start, stop), info)
+    new MarkupNode(start, stop, content.substring(start, stop), info, Nil)
   }
 
 
diff -r cc5d388fcbf2 -r 611864f2729d src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Sat Sep 05 00:35:37 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Sat Sep 05 00:43:59 2009 +0200
@@ -12,9 +12,8 @@
 import isabelle.proofdocument.ProofDocument
 
 
-class MarkupNode(val start: Int, val stop: Int,
-  val children: List[MarkupNode],
-  val content: String, val info: Any)
+class MarkupNode(val start: Int, val stop: Int, val content: String, val info: Any,
+  val children: List[MarkupNode])
 {
 
   def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode =
@@ -25,12 +24,12 @@
   }
 
   def set_children(new_children: List[MarkupNode]): MarkupNode =
-    new MarkupNode(start, stop, new_children, content, info)
+    new MarkupNode(start, stop, content, info, new_children)
 
   private def add(child: MarkupNode) =   // FIXME avoid sort?
     set_children ((child :: children) sort ((a, b) => a.start < b.start))
 
-  def remove(nodes: List[MarkupNode]) = set_children(children diff nodes)
+  def remove(nodes: List[MarkupNode]) = set_children(children -- nodes)
 
   def fits_into(node: MarkupNode): Boolean =
     node.start <= this.start && this.stop <= node.stop
@@ -65,14 +64,15 @@
         child <- children
         markups =
           if (next_x < child.start) {
-            new MarkupNode(next_x, child.start, Nil, content, info) :: child.flatten
+            // FIXME proper content!?
+            new MarkupNode(next_x, child.start, content, info, Nil) :: child.flatten
           }
           else child.flatten
         update = (next_x = child.stop)
         markup <- markups
       } yield markup
       if (next_x < stop)
-        filled_gaps + new MarkupNode(next_x, stop, Nil, content, info)
+        filled_gaps + new MarkupNode(next_x, stop, content, info, Nil) // FIXME proper content!?
       else filled_gaps
     }
   }