# HG changeset patch
# User wenzelm
# Date 1608388349 -3600
# Node ID 0d8bc0252e2ebe4c2ec476125a5c7c8080fb29f3
# Parent  75fc90edc0a86414c18b8ef8ab92b0c1eb5dfb09
tuned signature;

diff -r 75fc90edc0a8 -r 0d8bc0252e2e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 19 15:14:01 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 19 15:32:29 2020 +0100
@@ -592,7 +592,7 @@
 
     /* command as add-on snippet */
 
-    def command_snippet(command: Command): Snapshot =
+    def snippet(command: Command): Snapshot =
     {
       val node_name = command.node_name
 
@@ -998,8 +998,7 @@
             Command.unparsed(command.source, theory = true, id = id, node_name = node_name,
               blobs_info = command.blobs_info, results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - id)
-          val snapshot = state1.command_snippet(command1)
-          (snapshot, state1)
+          (state1.snippet(command1), state1)
       }
 
     def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
@@ -1252,7 +1251,7 @@
       new Snapshot(this, version, node_name, edits, snippet_command)
     }
 
-    def command_snippet(command: Command): Snapshot =
-      snapshot().command_snippet(command)
+    def snippet(command: Command): Snapshot =
+      snapshot().snippet(command)
   }
 }
diff -r 75fc90edc0a8 -r 0d8bc0252e2e src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Dec 19 15:14:01 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Dec 19 15:32:29 2020 +0100
@@ -120,7 +120,7 @@
             match {
               case None => progress.echo(thy_heading + " MISSING")
               case Some(command) =>
-                val snapshot = Document.State.init.command_snippet(command)
+                val snapshot = Document.State.init.snippet(command)
                 val rendering = new Rendering(snapshot, options, session)
                 val messages =
                   rendering.text_messages(Text.Range.full)
diff -r 75fc90edc0a8 -r 0d8bc0252e2e src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Dec 19 15:14:01 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sat Dec 19 15:32:29 2020 +0100
@@ -30,7 +30,7 @@
     results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) =
   {
     val command = Command.rich_text(Document_ID.make(), results, formatted_body)
-    val snippet = snapshot.command_snippet(command)
+    val snippet = snapshot.snippet(command)
     val model = File_Model.empty(PIDE.session)
     val rendering = apply(snippet, model, PIDE.options.value)
     (command.source, rendering)