src/Pure/System/isar.ML
changeset 51662 3391a493f39a
parent 50917 9459f59cff09
child 51948 cb5dbc9a06f9
     1.1 --- a/src/Pure/System/isar.ML	Tue Apr 09 15:59:02 2013 +0200
     1.2 +++ b/src/Pure/System/isar.ML	Tue Apr 09 20:16:52 2013 +0200
     1.3 @@ -118,6 +118,23 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun protocol_message props output =
     1.8 +  (case props of
     1.9 +    function :: args =>
    1.10 +      if function = Markup.command_timing then
    1.11 +        let
    1.12 +          val name = the_default "" (Properties.get args Markup.nameN);
    1.13 +          val pos = Position.of_properties args;
    1.14 +          val timing = Markup.parse_timing_properties args;
    1.15 +        in
    1.16 +          if Timing.is_relevant timing andalso (! Toplevel.profiling > 0 orelse ! Toplevel.timing)
    1.17 +            andalso name <> "" andalso not (Keyword.is_control name)
    1.18 +          then tracing ("command " ^ quote name ^ Position.here pos ^ ": " ^ Timing.message timing)
    1.19 +          else ()
    1.20 +        end
    1.21 +      else raise Output.Protocol_Message props
    1.22 +  | [] => raise Output.Protocol_Message props);
    1.23 +
    1.24  fun raw_loop secure src =
    1.25    let
    1.26      fun check_secure () =
    1.27 @@ -139,6 +156,7 @@
    1.28  fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
    1.29   (Context.set_thread_data NONE;
    1.30    if do_init then (Options.load_default (); init ()) else ();
    1.31 +  Output.Private_Hooks.protocol_message_fn := protocol_message;
    1.32    if welcome then writeln (Session.welcome ()) else ();
    1.33    uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
    1.34