--- 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
--- 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
}
--- 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()
--- 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)
--- 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)
{
--- 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)
}
}
--- 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
}