src/Pure/Tools/build.ML
changeset 66873 9953ae603a23
parent 66712 4c98c929a12a
child 67219 81e9804b2014
     1.1 --- a/src/Pure/Tools/build.ML	Mon Oct 16 14:21:14 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Mon Oct 16 14:32:09 2017 +0200
     1.3 @@ -92,6 +92,8 @@
     1.4              | NONE => ())
     1.5            else ()
     1.6          end
     1.7 +      else if function = Markup.theory_timing then
     1.8 +        inline_message (#2 function) args
     1.9        else
    1.10          (case Markup.dest_loading_theory props of
    1.11            SOME name => writeln ("\floading_theory = " ^ name)