Command: added name field and toString;
authorwenzelm
Tue Jan 20 22:55:45 2009 +0100 (2009-01-20 ago)
changeset 34495722533c532da
parent 34494 47f9303db81d
child 34496 1b2995592bb9
Command: added name field and toString;
src/Tools/jEdit/src/prover/Command.scala
     1.1 --- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 20 22:30:54 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 20 22:55:45 2009 +0100
     1.3 @@ -74,6 +74,9 @@
     1.4  
     1.5    /* content */
     1.6  
     1.7 +  override def toString = name
     1.8 +
     1.9 +  val name = text.content(first.start, first.stop)
    1.10    val content = text.content(proper_start, proper_stop)
    1.11  
    1.12    def next = if (last.next != null) last.next.command else null