diff -r 5f160df596c1 -r 60d0ee8f2ddb src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Sun Feb 17 22:15:02 2019 +0100 +++ b/src/Pure/System/progress.scala Mon Feb 18 15:57:06 2019 +0100 @@ -28,7 +28,7 @@ def echo(msg: String) {} def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) } def theory(theory: Progress.Theory) {} - def nodes_status(snapshot: Document.Snapshot, nodes_status: Document_Status.Nodes_Status) {} + def nodes_status(nodes_status: Document_Status.Nodes_Status) {} def echo_warning(msg: String) { echo(Output.warning_text(msg)) } def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }