src/Pure/Thy/thy_info.ML
changeset 66873 9953ae603a23
parent 66711 80fa1401cf76
child 67163 257bcd20eeec
     1.1 --- a/src/Pure/Thy/thy_info.ML	Mon Oct 16 14:21:14 2017 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Oct 16 14:32:09 2017 +0200
     1.3 @@ -301,10 +301,17 @@
     1.4        Execution.running Document_ID.none exec_id [] orelse
     1.5          raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
     1.6  
     1.7 +    val timing_start = Timing.start ();
     1.8 +
     1.9      val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
    1.10      val (theory, present, weight) =
    1.11        eval_thy document symbols last_timing update_time dir header text_pos text
    1.12          (if name = Context.PureN then [Context.the_global_context ()] else parents);
    1.13 +
    1.14 +    val timing_result = Timing.result timing_start;
    1.15 +    val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
    1.16 +    val _  = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
    1.17 +
    1.18      fun commit () = update_thy deps theory;
    1.19    in
    1.20      Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}