# HG changeset patch # User wenzelm # Date 1535997891 -7200 # Node ID b15b03c13dbb66a39919880a3a319ec3b2375231 # Parent 241d08beaf5c4f6b5527347047f047c477f39524 more detailed progress; diff -r 241d08beaf5c -r b15b03c13dbb src/Pure/System/progress.scala --- 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)) } diff -r 241d08beaf5c -r b15b03c13dbb src/Pure/Thy/thy_resources.scala --- 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 }) diff -r 241d08beaf5c -r b15b03c13dbb src/Pure/Tools/dump.scala --- 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 {