provide theory timing information, similar to command timing but always considered relevant;

--- a/src/Pure/Admin/build_log.scala	Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Mon Oct 16 14:32:09 2017 +0200
@@ -283,9 +283,11 @@
 
     def parse_session_info(
         command_timings: Boolean = false,
+        theory_timings: Boolean = false,
         ml_statistics: Boolean = false,
         task_statistics: Boolean = false): Session_Info =
-      Build_Log.parse_session_info(log_file, command_timings, ml_statistics, task_statistics)
+      Build_Log.parse_session_info(
+        log_file, command_timings, theory_timings, ml_statistics, task_statistics)
   }
 
 
@@ -446,6 +448,7 @@
 
   /** build info: toplevel output of isabelle build or Admin/build_history **/
 
+  val THEORY_TIMING_MARKER = "\ftheory_timing = "
   val ML_STATISTICS_MARKER = "\fML_statistics = "
   val ERROR_MESSAGE_MARKER = "\ferror_message = "
   val SESSION_NAME = "session_name"
@@ -612,6 +615,7 @@
   sealed case class Session_Info(
     session_timing: Properties.T,
     command_timings: List[Properties.T],
+    theory_timings: List[Properties.T],
     ml_statistics: List[Properties.T],
     task_statistics: List[Properties.T],
     errors: List[String])
@@ -619,12 +623,14 @@
   private def parse_session_info(
     log_file: Log_File,
     command_timings: Boolean,
+    theory_timings: Boolean,
     ml_statistics: Boolean,
     task_statistics: Boolean): Session_Info =
   {
     Session_Info(
       session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
       command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
+      theory_timings = if (theory_timings) log_file.filter_props(THEORY_TIMING_MARKER) else Nil,
       ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
       task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil,
       errors = log_file.filter_lines(ERROR_MESSAGE_MARKER).map(Library.decode_lines(_)))

--- a/src/Pure/PIDE/markup.ML	Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Oct 16 14:32:09 2017 +0200
@@ -194,6 +194,7 @@
   val ML_statistics: Properties.entry
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
+  val theory_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val build_session_finished: Properties.T
@@ -619,6 +620,8 @@
 
 val command_timing = (functionN, "command_timing");
 
+val theory_timing = (functionN, "theory_timing");
+
 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
 
 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name

--- a/src/Pure/PIDE/markup.scala	Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Oct 16 14:32:09 2017 +0200
@@ -392,9 +392,11 @@
   }
 
 
-  /* command timing */
+  /* protocol functions */
 
-  val COMMAND_TIMING = "command_timing"
+  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
+
+  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
 
 
   /* command indentation */

--- a/src/Pure/PIDE/protocol.scala	Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Oct 16 14:32:09 2017 +0200
@@ -113,7 +113,7 @@
   {
     def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
       props match {
-        case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
+        case Markup.COMMAND_TIMING :: args =>
           (args, args) match {
             case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
             case _ => None
@@ -123,6 +123,22 @@
   }
 
 
+  /* theory timing */
+
+  object Theory_Timing
+  {
+    def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
+      props match {
+        case Markup.THEORY_TIMING :: args =>
+          (args, args) match {
+            case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
+            case _ => None
+          }
+        case _ => None
+      }
+  }
+
+
   /* node status */
 
   sealed case class Node_Status(

--- a/src/Pure/PIDE/session.scala	Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/PIDE/session.scala	Mon Oct 16 14:32:09 2017 +0200
@@ -432,6 +432,9 @@
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
                 accumulate(state_id, xml_cache.elem(message))
 
+              case Protocol.Theory_Timing(_, _) =>
+                // FIXME
+
               case Markup.Assign_Update =>
                 msg.text match {
                   case Protocol.Assign_Update(id, update) =>

--- a/src/Pure/Thy/sessions.scala	Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Oct 16 14:32:09 2017 +0200
@@ -829,11 +829,13 @@
     // Build_Log.Session_Info
     val session_timing = SQL.Column.bytes("session_timing")
     val command_timings = SQL.Column.bytes("command_timings")
+    val theory_timings = SQL.Column.bytes("theory_timings")
     val ml_statistics = SQL.Column.bytes("ml_statistics")
     val task_statistics = SQL.Column.bytes("task_statistics")
     val errors = SQL.Column.bytes("errors")
     val build_log_columns =
-      List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
+      List(session_name, session_timing, command_timings, theory_timings,
+        ml_statistics, task_statistics, errors)
 
     // Build.Session_Info
     val sources = SQL.Column.string("sources")
@@ -926,13 +928,14 @@
           stmt.string(1) = name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
           stmt.bytes(3) = Properties.compress(build_log.command_timings)
-          stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
-          stmt.bytes(5) = Properties.compress(build_log.task_statistics)
-          stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
-          stmt.string(7) = build.sources
-          stmt.string(8) = cat_lines(build.input_heaps)
-          stmt.string(9) = build.output_heap getOrElse ""
-          stmt.int(10) = build.return_code
+          stmt.bytes(4) = Properties.compress(build_log.theory_timings)
+          stmt.bytes(5) = Properties.compress(build_log.ml_statistics)
+          stmt.bytes(6) = Properties.compress(build_log.task_statistics)
+          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors)
+          stmt.string(8) = build.sources
+          stmt.string(9) = cat_lines(build.input_heaps)
+          stmt.string(10) = build.output_heap getOrElse ""
+          stmt.int(11) = build.return_code
           stmt.execute()
         })
       }
@@ -944,6 +947,9 @@
     def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.command_timings)
 
+    def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
+      read_properties(db, name, Session_Info.theory_timings)
+
     def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
       read_properties(db, name, Session_Info.ml_statistics)
 

--- a/src/Pure/Thy/thy_info.ML	Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Oct 16 14:32:09 2017 +0200
@@ -301,10 +301,17 @@
       Execution.running Document_ID.none exec_id [] orelse
         raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
 
+    val timing_start = Timing.start ();
+
     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
     val (theory, present, weight) =
       eval_thy document symbols last_timing update_time dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
+
+    val timing_result = Timing.result timing_start;
+    val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
+    val _  = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
+
     fun commit () = update_thy deps theory;
   in
     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}

--- a/src/Pure/Tools/build.ML	Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/Tools/build.ML	Mon Oct 16 14:32:09 2017 +0200
@@ -92,6 +92,8 @@
             | NONE => ())
           else ()
         end
+      else if function = Markup.theory_timing then
+        inline_message (#2 function) args
       else
         (case Markup.dest_loading_theory props of
           SOME name => writeln ("\floading_theory = " ^ name)

--- a/src/Pure/Tools/build.scala	Mon Oct 16 14:21:14 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Oct 16 14:32:09 2017 +0200
@@ -537,7 +537,10 @@
                   build_log =
                     Build_Log.Log_File(name, process_result.out_lines).
                       parse_session_info(
-                        command_timings = true, ml_statistics = true, task_statistics = true),
+                        command_timings = true,
+                        theory_timings = true,
+                        ml_statistics = true,
+                        task_statistics = true),
                   build =
                     Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
                       process_result.rc)))