author | wenzelm |
Mon, 23 Jun 2025 13:41:18 +0200 | |
changeset 82738 | c4964970521e |
parent 82737 | 4694d8cce777 |
child 82739 | 0e0fee3599c2 |
--- 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")