clarified theory progress;
authorwenzelm
Sun Sep 09 11:53:53 2018 +0200 (14 months ago)
changeset 68957eef4e983fd9d
parent 68956 122c0d6cb790
child 68958 9199f9da512a
clarified theory progress;
src/Doc/System/Server.thy
src/Pure/System/progress.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/build.scala
src/Pure/Tools/server.scala
src/Tools/VSCode/src/channel.scala
src/Tools/jEdit/src/session_build.scala
     1.1 --- a/src/Doc/System/Server.thy	Sat Sep 08 22:52:12 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Sun Sep 09 11:53:53 2018 +0200
     1.3 @@ -477,11 +477,12 @@
     1.4    omitted in the command specifications below).
     1.5  
     1.6    \<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
     1.7 -  string, session: string}\<close> reports formal progress in loading theories (e.g.\
     1.8 -  when building a session image). Apart from a regular output message, it also
     1.9 -  reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
    1.10 -  \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
    1.11 -  e.g.\ theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
    1.12 +  string, session: string, percentage?: int}\<close> reports formal progress in
    1.13 +  loading theories (e.g.\ when building a session image). Apart from a regular
    1.14 +  output message, it also reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>)
    1.15 +  and session name (e.g.\ \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a
    1.16 +  proper session prefix, e.g.\ theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>. The
    1.17 +  optional percentage has the same meaning as in \<^bold>\<open>type\<close>~\<open>node_status\<close> below.
    1.18  
    1.19    \<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
    1.20    common Isabelle timing information in seconds, usually with a precision of
     2.1 --- a/src/Pure/System/progress.scala	Sat Sep 08 22:52:12 2018 +0200
     2.2 +++ b/src/Pure/System/progress.scala	Sun Sep 09 11:53:53 2018 +0200
     2.3 @@ -12,19 +12,19 @@
     2.4  
     2.5  object Progress
     2.6  {
     2.7 -  def theory_message(session: String, theory: String): String =
     2.8 -    if (session == "") "theory " + theory else session + ": theory " + theory
     2.9 -
    2.10 -  def theory_percentage_message(session: String, theory: String, percentage: Int): String =
    2.11 -    theory_message(session, theory) + ": " + percentage + "%"
    2.12 +  sealed case class Theory(theory: String, session: String = "", percentage: Option[Int] = None)
    2.13 +  {
    2.14 +    def message: String =
    2.15 +      (if (session == "") "theory " + theory else session + ": theory " + theory) +
    2.16 +      (percentage match { case None => "" case Some(p) => " " + p + "%" })
    2.17 +  }
    2.18  }
    2.19  
    2.20  class Progress
    2.21  {
    2.22    def echo(msg: String) {}
    2.23    def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
    2.24 -  def theory(session: String, theory: String) {}
    2.25 -  def theory_percentage(session: String, theory: String, percentage: Int) {}
    2.26 +  def theory(theory: Progress.Theory) {}
    2.27    def nodes_status(nodes_status: Document_Status.Nodes_Status) {}
    2.28  
    2.29    def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
    2.30 @@ -59,11 +59,8 @@
    2.31    override def echo(msg: String): Unit =
    2.32      Output.writeln(msg, stdout = !stderr)
    2.33  
    2.34 -  override def theory(session: String, theory: String): Unit =
    2.35 -    if (verbose) echo(Progress.theory_message(session, theory))
    2.36 -
    2.37 -  override def theory_percentage(session: String, theory: String, percentage: Int): Unit =
    2.38 -    if (verbose) echo(Progress.theory_percentage_message(session, theory, percentage))
    2.39 +  override def theory(theory: Progress.Theory): Unit =
    2.40 +    if (verbose) echo(theory.message)
    2.41  
    2.42    @volatile private var is_stopped = false
    2.43    override def interrupt_handler[A](e: => A): A =
    2.44 @@ -80,11 +77,8 @@
    2.45    override def echo(msg: String): Unit =
    2.46      File.append(path, msg + "\n")
    2.47  
    2.48 -  override def theory(session: String, theory: String): Unit =
    2.49 -    if (verbose) echo(Progress.theory_message(session, theory))
    2.50 -
    2.51 -  override def theory_percentage(session: String, theory: String, percentage: Int): Unit =
    2.52 -    if (verbose) echo(Progress.theory_percentage_message(session, theory, percentage))
    2.53 +  override def theory(theory: Progress.Theory): Unit =
    2.54 +    if (verbose) echo(theory.message)
    2.55  
    2.56    override def toString: String = path.toString
    2.57  }
     3.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Sep 08 22:52:12 2018 +0200
     3.2 +++ b/src/Pure/Thy/thy_resources.scala	Sun Sep 09 11:53:53 2018 +0200
     3.3 @@ -251,7 +251,7 @@
     3.4                val state = snapshot.state
     3.5                val version = snapshot.version
     3.6  
     3.7 -              val theory_percentages =
     3.8 +              val theory_progress =
     3.9                  use_theories_state.change_result(st =>
    3.10                    {
    3.11                      val domain =
    3.12 @@ -266,19 +266,18 @@
    3.13                        delay_nodes_status.invoke
    3.14                      }
    3.15  
    3.16 -                    val progress_percentage =
    3.17 +                    val theory_progress =
    3.18                        (for {
    3.19                          (name, node_status) <- nodes_status1.present.iterator
    3.20 -                        if changed.nodes.contains(name)
    3.21 -                        p1 = node_status.percentage
    3.22 -                        if Some(p1) != st.nodes_status.get(name).map(_.percentage)
    3.23 -                      } yield (name.theory, p1)).toList
    3.24 +                        if changed.nodes.contains(name) && !version.nodes(name).is_empty
    3.25 +                        percentage = Some(node_status.percentage)
    3.26 +                        if percentage != st.nodes_status.get(name).map(_.percentage)
    3.27 +                      } yield Progress.Theory(name.theory, percentage = percentage)).toList
    3.28  
    3.29 -                    (progress_percentage, st.update(nodes_status1))
    3.30 +                    (theory_progress, st.update(nodes_status1))
    3.31                    })
    3.32  
    3.33 -              for ((theory, percentage) <- theory_percentages)
    3.34 -                progress.theory_percentage("", theory, percentage)
    3.35 +              theory_progress.foreach(progress.theory(_))
    3.36  
    3.37                check_result()
    3.38  
     4.1 --- a/src/Pure/Tools/build.scala	Sat Sep 08 22:52:12 2018 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Sun Sep 09 11:53:53 2018 +0200
     4.3 @@ -170,7 +170,7 @@
     4.4      private def loading_theory(msg: Prover.Protocol_Output): Boolean =
     4.5        msg.properties match {
     4.6          case Markup.Loading_Theory(name) =>
     4.7 -          progress.theory(session_name, name)
     4.8 +          progress.theory(Progress.Theory(name, session = session_name))
     4.9            true
    4.10          case _ => false
    4.11        }
    4.12 @@ -291,7 +291,8 @@
    4.13            process.result(
    4.14              progress_stdout = (line: String) =>
    4.15                Library.try_unprefix("\floading_theory = ", line) match {
    4.16 -                case Some(theory) => progress.theory(name, theory)
    4.17 +                case Some(theory) =>
    4.18 +                  progress.theory(Progress.Theory(theory, session = name))
    4.19                  case None =>
    4.20                    for {
    4.21                      text <- Library.try_unprefix("\fexport = ", line)
     5.1 --- a/src/Pure/Tools/server.scala	Sat Sep 08 22:52:12 2018 +0200
     5.2 +++ b/src/Pure/Tools/server.scala	Sun Sep 09 11:53:53 2018 +0200
     5.3 @@ -269,9 +269,13 @@
     5.4      override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
     5.5      override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
     5.6  
     5.7 -    override def theory(session: String, theory: String): Unit =
     5.8 -      context.writeln(Progress.theory_message(session, theory),
     5.9 -        (List("session" -> session, "theory" -> theory) ::: more.toList):_*)
    5.10 +    override def theory(theory: Progress.Theory)
    5.11 +    {
    5.12 +      val entries: List[JSON.Object.Entry] =
    5.13 +        List("theory" -> theory.theory, "session" -> theory.session) :::
    5.14 +          (theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) })
    5.15 +      context.writeln(theory.message, entries ::: more.toList:_*)
    5.16 +    }
    5.17  
    5.18      override def nodes_status(nodes_status: Document_Status.Nodes_Status)
    5.19      {
     6.1 --- a/src/Tools/VSCode/src/channel.scala	Sat Sep 08 22:52:12 2018 +0200
     6.2 +++ b/src/Tools/VSCode/src/channel.scala	Sun Sep 09 11:53:53 2018 +0200
     6.3 @@ -103,7 +103,6 @@
     6.4        override def echo(msg: String): Unit = log_writeln(msg)
     6.5        override def echo_warning(msg: String): Unit = log_warning(msg)
     6.6        override def echo_error_message(msg: String): Unit = log_error_message(msg)
     6.7 -      override def theory(session: String, theory: String): Unit =
     6.8 -        if (verbose) echo(Progress.theory_message(session, theory))
     6.9 +      override def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message)
    6.10      }
    6.11  }
     7.1 --- a/src/Tools/jEdit/src/session_build.scala	Sat Sep 08 22:52:12 2018 +0200
     7.2 +++ b/src/Tools/jEdit/src/session_build.scala	Sun Sep 09 11:53:53 2018 +0200
     7.3 @@ -67,8 +67,7 @@
     7.4            vertical.setValue(vertical.getMaximum)
     7.5          }
     7.6  
     7.7 -      override def theory(session: String, theory: String): Unit =
     7.8 -        echo(Progress.theory_message(session, theory))
     7.9 +      override def theory(theory: Progress.Theory): Unit = echo(theory.message)
    7.10  
    7.11        override def stopped: Boolean = is_stopped
    7.12      }