src/Pure/PIDE/document.scala
changeset 72722 ade53fbc6f03
parent 72721 79f5e843e5ec
child 72723 3b804e0ffae9
--- 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)