--- 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)
}
}
--- 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(