# HG changeset patch
# User wenzelm
# Date 1252102030 -7200
# Node ID cd2cdf3b33b9eb8490821145e61c017d721811c8
# Parent  504cab625d3e6f2197604cf6ccfd807db35e1963
MarkupNode: removed id;

diff -r 504cab625d3e -r cd2cdf3b33b9 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Fri Sep 04 23:43:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Sat Sep 05 00:07:10 2009 +0200
@@ -46,18 +46,20 @@
                 new Position { def getOffset = offset; override def toString = offset.toString }
 
               val command_start = command.start(document)
+              val id = command.id
+
               new DefaultMutableTreeNode(new IAsset {
                 override def getIcon: Icon = null
                 override def getShortString: String = node.content
                 override def getLongString: String = node.info.toString
-                override def getName: String = node.id
+                override def getName: String = id
                 override def setName(name: String) = ()
                 override def setStart(start: Position) = ()
                 override def getStart: Position = command_start + node.start
                 override def setEnd(end: Position) = ()
                 override def getEnd: Position = command_start + node.stop
                 override def toString =
-                  node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
+                  id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
               })
             }))
       }
diff -r 504cab625d3e -r cd2cdf3b33b9 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Fri Sep 04 23:43:42 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sat Sep 05 00:07:10 2009 +0200
@@ -79,13 +79,13 @@
 
   lazy val empty_root_node =
     new MarkupNode(0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
-      Nil, id, content, RootInfo())
+      Nil, content, RootInfo())
 
   def markup_node(begin: Int, end: Int, info: MarkupInfo): MarkupNode =
   {
     val start = symbol_index.decode(begin)
     val stop = symbol_index.decode(end)
-    new MarkupNode(start, stop, Nil, id, content.substring(start, stop), info)
+    new MarkupNode(start, stop, Nil, content.substring(start, stop), info)
   }
 
 
diff -r 504cab625d3e -r cd2cdf3b33b9 src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri Sep 04 23:43:42 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Sat Sep 05 00:07:10 2009 +0200
@@ -26,7 +26,7 @@
 
 class MarkupNode(val start: Int, val stop: Int,
   val children: List[MarkupNode],
-  val id: String, val content: String, val info: MarkupInfo)
+  val content: String, val info: MarkupInfo)
 {
 
   def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode =
@@ -37,7 +37,7 @@
   }
 
   def set_children(new_children: List[MarkupNode]): MarkupNode =
-    new MarkupNode(start, stop, new_children, id, content, info)
+    new MarkupNode(start, stop, new_children, content, info)
 
   private def add(child: MarkupNode) =   // FIXME avoid sort?
     set_children ((child :: children) sort ((a, b) => a.start < b.start))
@@ -91,14 +91,14 @@
         child <- children
         markups =
           if (next_x < child.start) {
-            new MarkupNode(next_x, child.start, Nil, id, content, info) :: child.flatten
+            new MarkupNode(next_x, child.start, Nil, content, info) :: 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, id, content, info)
+        filled_gaps + new MarkupNode(next_x, stop, Nil, content, info)
       else filled_gaps
     }
   }
@@ -111,5 +111,5 @@
   }
 
   override def toString =
-    "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
+    "([" + start + " - " + stop + "] ( " + content + "): " + info.toString
 }