--- a/src/Tools/jEdit/src/prover/Command.scala Thu Sep 03 20:10:23 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Fri Sep 04 23:04:20 2009 +0200
@@ -83,9 +83,9 @@
def markup_node(begin: Int, end: Int, info: MarkupInfo): MarkupNode =
{
- new MarkupNode(this, symbol_index.decode(begin), symbol_index.decode(end), Nil, id,
- content.substring(symbol_index.decode(begin), symbol_index.decode(end)),
- info)
+ val start = symbol_index.decode(begin)
+ val stop = symbol_index.decode(end)
+ new MarkupNode(this, start, stop, Nil, id, content.substring(start, stop), info)
}