author | immler@in.tum.de |
Sat, 24 Jan 2009 16:31:04 +0100 | |
changeset 34510 | 6106e71c6ee5 |
parent 34496 | 1b2995592bb9 |
child 34511 | 5839e34ef0bd |
--- a/src/Tools/jEdit/src/prover/Command.scala Tue Jan 20 23:13:54 2009 +0100 +++ b/src/Tools/jEdit/src/prover/Command.scala Sat Jan 24 16:31:04 2009 +0100 @@ -100,7 +100,7 @@ new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content) def node_from(kind: String, begin: Int, end: Int) = { - val markup_content = /*content.substring(begin, end)*/ "" + val markup_content = content.substring(begin, end) new MarkupNode(this, begin, end, id, kind, markup_content) } }