# HG changeset patch
# User wenzelm
# Date 1750678878 -7200
# Node ID c4964970521e20365d0c77f136033c19bca30b8f
# Parent  4694d8cce777feb5a1c806274f0b1d22214839d4
tuned comments;

diff -r 4694d8cce777 -r c4964970521e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Jun 23 12:42:53 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Jun 23 13:41:18 2025 +0200
@@ -626,7 +626,7 @@
       } yield convert(cmd.core_range + start)).toList
 
 
-    /* command as add-on snippet */
+    /* add-on snippet via pro-forma commands */
 
     def snippet(commands: List[Command], doc_blobs: Blobs): Snapshot = {
       require(commands.nonEmpty, "no snippet commands")