src/Pure/PIDE/document.scala
changeset 72859 2b8a328138a6
parent 72844 240c8a0f6337
child 72860 64378eaf393d
--- a/src/Pure/PIDE/document.scala	Wed Dec 09 20:10:10 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Dec 09 20:19:27 2020 +0100
@@ -998,7 +998,7 @@
             Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name,
               blobs_info = command.blobs_info, results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - command1.id)
-          val snapshot = state1.snapshot(node_name = node_name).command_snippet(command1)
+          val snapshot = state1.command_snippet(command1)
           (snapshot, state1)
       }
 
@@ -1253,5 +1253,8 @@
 
       new Snapshot(this, version, node_name, edits, snippet_command)
     }
+
+    def command_snippet(command: Command): Snapshot =
+      snapshot().command_snippet(command)
   }
 }