src/Pure/Tools/build.ML
changeset 68090 0763d4eb3ebc
parent 67493 c4e9e0c50487
child 68148 fb661e4c4717
     1.1 --- a/src/Pure/Tools/build.ML	Sat May 05 21:44:18 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Sat May 05 22:33:35 2018 +0200
     1.3 @@ -94,6 +94,10 @@
     1.4          end
     1.5        else if function = Markup.theory_timing then
     1.6          inline_message (#2 function) args
     1.7 +      else if function = (Markup.functionN, Markup.exportN) andalso
     1.8 +        not (null args) andalso #1 (hd args) = Markup.idN
     1.9 +      then
    1.10 +        inline_message (#2 function) (tl args @ [(Markup.exportN, hex_string (implode output))])
    1.11        else
    1.12          (case Markup.dest_loading_theory props of
    1.13            SOME name => writeln ("\floading_theory = " ^ name)