# HG changeset patch # User wenzelm # Date 1607541567 -3600 # Node ID 2b8a328138a6fa0a6904295f6e6893e83f136958 # Parent cb0c407fbc6eb4eaf5e033e4ec5c26b55817081f clarified signature; diff -r cb0c407fbc6e -r 2b8a328138a6 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Dec 09 20:10:10 2020 +0100 +++ b/src/Pure/PIDE/document.scala Wed Dec 09 20:19:27 2020 +0100 @@ -998,7 +998,7 @@ Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name, blobs_info = command.blobs_info, results = st.results, markups = st.markups) val state1 = copy(theories = theories - command1.id) - val snapshot = state1.snapshot(node_name = node_name).command_snippet(command1) + val snapshot = state1.command_snippet(command1) (snapshot, state1) } @@ -1253,5 +1253,8 @@ new Snapshot(this, version, node_name, edits, snippet_command) } + + def command_snippet(command: Command): Snapshot = + snapshot().command_snippet(command) } } diff -r cb0c407fbc6e -r 2b8a328138a6 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Wed Dec 09 20:10:10 2020 +0100 +++ b/src/Pure/Tools/build_job.scala Wed Dec 09 20:19:27 2020 +0100 @@ -107,7 +107,7 @@ case None => progress.echo(thy_heading + ": MISSING") case Some(command) => progress.echo(thy_heading) - val snapshot = Document.State.init.snapshot().command_snippet(command) + val snapshot = Document.State.init.command_snippet(command) val rendering = new Rendering(snapshot, options, session) for (Text.Info(_, t) <- rendering.text_messages(Text.Range.full)) { progress.echo(