# HG changeset patch
# User wenzelm
# Date 1536486833 -7200
# Node ID eef4e983fd9d37b7e7b4c574c90babe9ebb8876b
# Parent  122c0d6cb7904e9ea27fafca80d4ad3293ddb2da
clarified theory progress;

diff -r 122c0d6cb790 -r eef4e983fd9d src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat Sep 08 22:52:12 2018 +0200
+++ b/src/Doc/System/Server.thy	Sun Sep 09 11:53:53 2018 +0200
@@ -477,11 +477,12 @@
   omitted in the command specifications below).
 
   \<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
-  string, session: string}\<close> reports formal progress in loading theories (e.g.\
-  when building a session image). Apart from a regular output message, it also
-  reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
-  \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
-  e.g.\ theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
+  string, session: string, percentage?: int}\<close> reports formal progress in
+  loading theories (e.g.\ when building a session image). Apart from a regular
+  output message, it also reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>)
+  and session name (e.g.\ \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a
+  proper session prefix, e.g.\ theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>. The
+  optional percentage has the same meaning as in \<^bold>\<open>type\<close>~\<open>node_status\<close> below.
 
   \<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
   common Isabelle timing information in seconds, usually with a precision of
diff -r 122c0d6cb790 -r eef4e983fd9d src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Sep 08 22:52:12 2018 +0200
+++ b/src/Pure/System/progress.scala	Sun Sep 09 11:53:53 2018 +0200
@@ -12,19 +12,19 @@
 
 object Progress
 {
-  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 + "%"
+  sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None)
+  {
+    def message: String =
+      (if (session == "") "theory " + theory else session + ": theory " + theory) +
+      (percentage match { case None => "" case Some(p) => " " + p + "%" })
+  }
 }
 
 class Progress
 {
   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 theory(theory: Progress.Theory) {}
   def nodes_status(nodes_status: Document_Status.Nodes_Status) {}
 
   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
@@ -59,11 +59,8 @@
   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))
+  override def theory(theory: Progress.Theory): Unit =
+    if (verbose) echo(theory.message)
 
   @volatile private var is_stopped = false
   override def interrupt_handler[A](e: => A): A =
@@ -80,11 +77,8 @@
   override def echo(msg: String): Unit =
     File.append(path, msg + "\n")
 
-  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 theory(theory: Progress.Theory): Unit =
+    if (verbose) echo(theory.message)
 
   override def toString: String = path.toString
 }
diff -r 122c0d6cb790 -r eef4e983fd9d src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 22:52:12 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Sun Sep 09 11:53:53 2018 +0200
@@ -251,7 +251,7 @@
               val state = snapshot.state
               val version = snapshot.version
 
-              val theory_percentages =
+              val theory_progress =
                 use_theories_state.change_result(st =>
                   {
                     val domain =
@@ -266,19 +266,18 @@
                       delay_nodes_status.invoke
                     }
 
-                    val progress_percentage =
+                    val theory_progress =
                       (for {
                         (name, node_status) <- nodes_status1.present.iterator
-                        if changed.nodes.contains(name)
-                        p1 = node_status.percentage
-                        if Some(p1) != st.nodes_status.get(name).map(_.percentage)
-                      } yield (name.theory, p1)).toList
+                        if changed.nodes.contains(name) && !version.nodes(name).is_empty
+                        percentage = Some(node_status.percentage)
+                        if percentage != st.nodes_status.get(name).map(_.percentage)
+                      } yield Progress.Theory(name.theory, percentage = percentage)).toList
 
-                    (progress_percentage, st.update(nodes_status1))
+                    (theory_progress, st.update(nodes_status1))
                   })
 
-              for ((theory, percentage) <- theory_percentages)
-                progress.theory_percentage("", theory, percentage)
+              theory_progress.foreach(progress.theory(_))
 
               check_result()
 
diff -r 122c0d6cb790 -r eef4e983fd9d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Sep 08 22:52:12 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sun Sep 09 11:53:53 2018 +0200
@@ -170,7 +170,7 @@
     private def loading_theory(msg: Prover.Protocol_Output): Boolean =
       msg.properties match {
         case Markup.Loading_Theory(name) =>
-          progress.theory(session_name, name)
+          progress.theory(Progress.Theory(name, session = session_name))
           true
         case _ => false
       }
@@ -291,7 +291,8 @@
           process.result(
             progress_stdout = (line: String) =>
               Library.try_unprefix("\floading_theory = ", line) match {
-                case Some(theory) => progress.theory(name, theory)
+                case Some(theory) =>
+                  progress.theory(Progress.Theory(theory, session = name))
                 case None =>
                   for {
                     text <- Library.try_unprefix("\fexport = ", line)
diff -r 122c0d6cb790 -r eef4e983fd9d src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Sat Sep 08 22:52:12 2018 +0200
+++ b/src/Pure/Tools/server.scala	Sun Sep 09 11:53:53 2018 +0200
@@ -269,9 +269,13 @@
     override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
     override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
 
-    override def theory(session: String, theory: String): Unit =
-      context.writeln(Progress.theory_message(session, theory),
-        (List("session" -> session, "theory" -> theory) ::: more.toList):_*)
+    override def theory(theory: Progress.Theory)
+    {
+      val entries: List[JSON.Object.Entry] =
+        List("theory" -> theory.theory, "session" -> theory.session) :::
+          (theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) })
+      context.writeln(theory.message, entries ::: more.toList:_*)
+    }
 
     override def nodes_status(nodes_status: Document_Status.Nodes_Status)
     {
diff -r 122c0d6cb790 -r eef4e983fd9d src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Sat Sep 08 22:52:12 2018 +0200
+++ b/src/Tools/VSCode/src/channel.scala	Sun Sep 09 11:53:53 2018 +0200
@@ -103,7 +103,6 @@
       override def echo(msg: String): Unit = log_writeln(msg)
       override def echo_warning(msg: String): Unit = log_warning(msg)
       override def echo_error_message(msg: String): Unit = log_error_message(msg)
-      override def theory(session: String, theory: String): Unit =
-        if (verbose) echo(Progress.theory_message(session, theory))
+      override def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message)
     }
 }
diff -r 122c0d6cb790 -r eef4e983fd9d src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sat Sep 08 22:52:12 2018 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sun Sep 09 11:53:53 2018 +0200
@@ -67,8 +67,7 @@
           vertical.setValue(vertical.getMaximum)
         }
 
-      override def theory(session: String, theory: String): Unit =
-        echo(Progress.theory_message(session, theory))
+      override def theory(theory: Progress.Theory): Unit = echo(theory.message)
 
       override def stopped: Boolean = is_stopped
     }