src/Pure/System/progress.scala

 
 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 + "%"
 }
 
 class Progress
 {
   def echo(msg: String) {}

 
 object No_Progress extends Progress
 
 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 }
   override def stopped: Boolean =

     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 toString: String = path.toString
 }