# HG changeset patch
# User wenzelm
# Date 1536436106 -7200
# Node ID a7b1fe2d30ad538e15243066e15df51070d854b0
# Parent  53f7b6b9f73422750166af6a96c0d5e3fc0b5367
more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session;

diff -r 53f7b6b9f734 -r a7b1fe2d30ad src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Sep 08 16:55:38 2018 +0200
+++ b/src/Pure/System/progress.scala	Sat Sep 08 21:48:26 2018 +0200
@@ -14,6 +14,9 @@
 {
   def theory_message(session: String, theory: String): String =
     if (session == "") "theory " + theory else session + ": theory " + theory
+
+  def theory_percentage_message(session: String, theory: String, percentage: Int): String =
+    theory_message(session, theory) + ": " + percentage + "%"
 }
 
 class Progress
@@ -53,14 +56,15 @@
 
 class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
 {
-  override def echo(msg: String)
-  {
+  override def echo(msg: String): Unit =
     Output.writeln(msg, stdout = !stderr)
-  }
 
   override def theory(session: String, theory: String): Unit =
     if (verbose) echo(Progress.theory_message(session, theory))
 
+  override def theory_percentage(session: String, theory: String, percentage: Int): Unit =
+    if (verbose) echo(Progress.theory_percentage_message(session, theory, percentage))
+
   @volatile private var is_stopped = false
   override def interrupt_handler[A](e: => A): A =
     POSIX_Interrupt.handler { is_stopped = true } { e }
@@ -79,5 +83,8 @@
   override def theory(session: String, theory: String): Unit =
     if (verbose) echo(Progress.theory_message(session, theory))
 
+  override def theory_percentage(session: String, theory: String, percentage: Int): Unit =
+    if (verbose) echo(Progress.theory_percentage_message(session, theory, percentage))
+
   override def toString: String = path.toString
 }
diff -r 53f7b6b9f734 -r a7b1fe2d30ad src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 16:55:38 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Sat Sep 08 21:48:26 2018 +0200
@@ -114,7 +114,6 @@
     private sealed case class Use_Theories_State(
       last_update: Time = Time.now(),
       nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
-      already_initialized: Set[Document.Node.Name] = Set.empty,
       already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
       result: Promise[Theories_Result] = Future.promise[Theories_Result])
     {
@@ -124,20 +123,6 @@
       def watchdog(watchdog_timeout: Time): Boolean =
         watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
 
-      def initialized_theories(
-        state: Document.State,
-        version: Document.Version,
-        theories: List[Document.Node.Name]): (List[Document.Node.Name], Use_Theories_State) =
-      {
-        val initialized =
-          for {
-            name <- theories
-            if !already_initialized(name) &&
-              Document_Status.Node_Status.make(state, version, name).initialized
-          } yield name
-        (initialized, copy(already_initialized = already_initialized ++ initialized))
-      }
-
       def cancel_result { result.cancel }
       def finished_result: Boolean = result.is_finished
       def await_result { result.join_result }
@@ -285,25 +270,12 @@
                         (name, node_status) <- nodes_status1.present.iterator
                         if changed.nodes.contains(name)
                         p1 = node_status.percentage
-                        if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
+                        if Some(p1) != st.nodes_status.get(name).map(_.percentage)
                       } yield (name.theory, p1)).toList
 
                     (progress_percentage, st.update(nodes_status1))
                   })
 
-              val check_theories =
-                (for {
-                  command <- changed.commands.iterator
-                  if dep_theories_set(command.node_name) && command.potentially_initialized
-                } yield command.node_name).toList
-
-              if (check_theories.nonEmpty) {
-                val initialized =
-                  use_theories_state.change_result(
-                    _.initialized_theories(state, version, check_theories))
-                initialized.map(_.theory).sorted.foreach(progress.theory("", _))
-              }
-
               for ((theory, percentage) <- theory_percentages)
                 progress.theory_percentage("", theory, percentage)
 
diff -r 53f7b6b9f734 -r a7b1fe2d30ad src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Sep 08 16:55:38 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Sat Sep 08 21:48:26 2018 +0200
@@ -242,13 +242,7 @@
 
       val sessions = getopts(args)
 
-      val progress = new Console_Progress()
-      {
-        override def theory_percentage(session: String, theory: String, percentage: Int)
-        {
-          if (verbose) echo(Progress.theory_message(session, theory) + ": " + percentage + "%")
-        }
-      }
+      val progress = new Console_Progress(verbose = verbose)
 
       val result =
         progress.interrupt_handler {