# 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 {