--- a/src/Pure/PIDE/markup_tree.scala Thu Aug 19 22:04:20 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Thu Aug 19 22:26:15 2010 +0200
@@ -50,6 +50,12 @@
{
import Markup_Tree._
+ override def toString =
+ branches.toList.map(_._2) match {
+ case Nil => "Empty"
+ case list => list.mkString("Tree(", ",", ")")
+ }
+
def + (new_node: Node): Markup_Tree =
{
branches.get(new_node) match {
--- a/src/Pure/PIDE/text.scala Thu Aug 19 22:04:20 2010 +0200
+++ b/src/Pure/PIDE/text.scala Thu Aug 19 22:26:15 2010 +0200
@@ -21,6 +21,8 @@
{
require(start <= stop)
+ override def toString = "[" + start.toString + ":" + stop.toString + "]"
+
def map(f: Offset => Offset): Range = Range(f(start), f(stop))
def +(i: Offset): Range = map(_ + i)
def contains(i: Offset): Boolean = start <= i && i < stop