# 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)