author | immler@in.tum.de |
Sun, 01 Feb 2009 12:21:07 +0100 | |
changeset 34511 | 5839e34ef0bd |
parent 34510 | 6106e71c6ee5 (diff) |
parent 34509 | 839d1f0b2dd1 (current diff) |
child 34512 | 14d70378f1c7 |
--- a/src/Tools/jEdit/src/prover/Command.scala Tue Jan 27 22:23:45 2009 +0100 +++ b/src/Tools/jEdit/src/prover/Command.scala Sun Feb 01 12:21:07 2009 +0100 @@ -103,7 +103,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) } }