diff -r 79f5e843e5ec -r ade53fbc6f03 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Nov 26 15:49:27 2020 +0100 +++ b/src/Pure/PIDE/document.scala Thu Nov 26 15:59:09 2020 +0100 @@ -822,7 +822,7 @@ val node_name = command.node_name val command1 = Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name, - results = st.results, markup = st.markup(Command.Markup_Index.markup)) + results = st.results, markups = st.markups) val state1 = copy(theories = theories - command1.id) val snapshot = state1.snapshot(name = node_name).command_snippet(command1) (snapshot, state1)