diff -r 4fa1aa5dac4f -r 59a7f82a7180 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Nov 26 13:15:57 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Nov 26 14:48:22 2020 +0100
@@ -552,6 +552,26 @@
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
 
+    def command_snippet(command: Command): Snapshot =
+    {
+      val node_name = command.node_name
+
+      val nodes0 = version.nodes
+      val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
+      val version1 = Document.Version.make(nodes1)
+
+      val edits: List[Edit_Text] =
+        List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source))))
+
+      val state0 = state.define_command(command)
+      val state1 =
+        state0.continue_history(Future.value(version), edits, Future.value(version1))
+          .define_version(version1, state0.the_assignment(version))
+          .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
+
+      state1.snapshot()
+    }
+
     def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
     def messages: List[(XML.Tree, Position.T)]
     def exports: List[Export.Entry]