equal
deleted
inserted
replaced
36 /* content */ |
36 /* content */ |
37 |
37 |
38 override def toString = name |
38 override def toString = name |
39 |
39 |
40 val name = tokens.head.content |
40 val name = tokens.head.content |
41 val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT), starts) |
41 val content:String = Token.string_from_tokens(tokens, starts) |
42 |
42 |
43 def start(doc: ProofDocument) = doc.token_start(tokens.first) |
43 def start(doc: ProofDocument) = doc.token_start(tokens.first) |
44 def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length |
44 def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length |
45 |
45 |
46 /* command status */ |
46 /* command status */ |