--- a/src/Pure/System/progress.scala Mon Sep 03 19:44:10 2018 +0200
+++ b/src/Pure/System/progress.scala Mon Sep 03 20:04:51 2018 +0200
@@ -21,6 +21,7 @@
def echo(msg: String) {}
def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
def theory(session: String, theory: String) {}
+ def theory_percentage(session: String, theory: String, percentage: Int) {}
def nodes_status(nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name]) {}
def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
--- a/src/Pure/Thy/thy_resources.scala Mon Sep 03 19:44:10 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala Mon Sep 03 20:04:51 2018 +0200
@@ -173,11 +173,21 @@
val domain =
if (nodes_status.is_empty) dep_theories_set
else changed.nodes.iterator.filter(dep_theories_set).toSet
- val upd1 =
+
+ val upd1 @ (nodes_status1, names1) =
nodes_status.update(resources.session_base, state, version,
domain = Some(domain), trim = changed.assignment).getOrElse(upd)
- if (nodes_status_delay >= Time.zero && upd != upd1)
+
+ for {
+ name <- names1.iterator if changed.nodes.contains(name)
+ p = nodes_status.get(name).map(_.percentage)
+ p1 = nodes_status1.get(name).map(_.percentage)
+ if p != p1 && p1.isDefined && p1.get > 0
+ } progress.theory_percentage("", name.theory, p1.get)
+
+ if (nodes_status_delay >= Time.zero && upd != upd1) {
delay_nodes_status.invoke
+ }
upd1
})
--- a/src/Pure/Tools/dump.scala Mon Sep 03 19:44:10 2018 +0200
+++ b/src/Pure/Tools/dump.scala Mon Sep 03 20:04:51 2018 +0200
@@ -206,6 +206,12 @@
val sessions = getopts(args)
val progress = new Console_Progress(verbose = verbose)
+ {
+ override def theory_percentage(session: String, theory: String, percentage: Int)
+ {
+ if (verbose) echo(Progress.theory_message(session, theory) + ": " + percentage + "%")
+ }
+ }
val result =
progress.interrupt_handler {