--- a/src/Tools/jEdit/src/prover/Command.scala Mon Jul 27 15:51:12 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala Mon Jul 27 15:51:37 2009 +0200
@@ -98,7 +98,7 @@
def add_markup(state: IsarDocument.State_ID, raw_node: MarkupNode) = {
// decode node
val node = raw_node transform symbol_index.decode
- if (state == null) _markup_root = _markup_root.add(node)
+ if (state == null) _markup_root += node
else {
val cmd_state = states.getOrElseUpdate(state, new Command_State(this))
cmd_state.markup_root += node