more detailed progress;
authorwenzelm
Mon Sep 03 20:04:51 2018 +0200 (9 months ago)
changeset 68899b15b03c13dbb
parent 68898 241d08beaf5c
child 68900 1145b25c53de
more detailed progress;
src/Pure/System/progress.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/System/progress.scala	Mon Sep 03 19:44:10 2018 +0200
     1.2 +++ b/src/Pure/System/progress.scala	Mon Sep 03 20:04:51 2018 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    def echo(msg: String) {}
     1.5    def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
     1.6    def theory(session: String, theory: String) {}
     1.7 +  def theory_percentage(session: String, theory: String, percentage: Int) {}
     1.8    def nodes_status(nodes_status: Document_Status.Nodes_Status, names: List[Document.Node.Name]) {}
     1.9  
    1.10    def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Mon Sep 03 19:44:10 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Mon Sep 03 20:04:51 2018 +0200
     2.3 @@ -173,11 +173,21 @@
     2.4                      val domain =
     2.5                        if (nodes_status.is_empty) dep_theories_set
     2.6                        else changed.nodes.iterator.filter(dep_theories_set).toSet
     2.7 -                    val upd1 =
     2.8 +
     2.9 +                    val upd1 @ (nodes_status1, names1) =
    2.10                        nodes_status.update(resources.session_base, state, version,
    2.11                          domain = Some(domain), trim = changed.assignment).getOrElse(upd)
    2.12 -                    if (nodes_status_delay >= Time.zero && upd != upd1)
    2.13 +
    2.14 +                    for {
    2.15 +                      name <- names1.iterator if changed.nodes.contains(name)
    2.16 +                      p = nodes_status.get(name).map(_.percentage)
    2.17 +                      p1 = nodes_status1.get(name).map(_.percentage)
    2.18 +                      if p != p1 && p1.isDefined && p1.get > 0
    2.19 +                    } progress.theory_percentage("", name.theory, p1.get)
    2.20 +
    2.21 +                    if (nodes_status_delay >= Time.zero && upd != upd1) {
    2.22                        delay_nodes_status.invoke
    2.23 +                    }
    2.24  
    2.25                      upd1
    2.26                  })
     3.1 --- a/src/Pure/Tools/dump.scala	Mon Sep 03 19:44:10 2018 +0200
     3.2 +++ b/src/Pure/Tools/dump.scala	Mon Sep 03 20:04:51 2018 +0200
     3.3 @@ -206,6 +206,12 @@
     3.4        val sessions = getopts(args)
     3.5  
     3.6        val progress = new Console_Progress(verbose = verbose)
     3.7 +      {
     3.8 +        override def theory_percentage(session: String, theory: String, percentage: Int)
     3.9 +        {
    3.10 +          if (verbose) echo(Progress.theory_message(session, theory) + ": " + percentage + "%")
    3.11 +        }
    3.12 +      }
    3.13  
    3.14        val result =
    3.15          progress.interrupt_handler {