# HG changeset patch
# User krauss
# Date 1333608211 -7200
# Node ID 4193098c4ec1321d5a698f928bda9ddd5bda4f56
# Parent  eabfb53cfca809e43ea21fc32c07d80b2befa51c
added timestamps to logging of named thms

diff -r eabfb53cfca8 -r 4193098c4ec1 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Thu Apr 05 08:13:40 2012 +0200
+++ b/src/HOL/Import/import_rule.ML	Thu Apr 05 08:43:31 2012 +0200
@@ -339,6 +339,14 @@
     snd (Global_Theory.add_thm ((binding, thm'), []) thy)
   end
 
+fun log_timestamp () =
+  let
+    val time = Time.now ()
+    val millis = nth (space_explode "." (Time.fmt 3 time)) 1
+  in
+    Date.fmt "%d.%m.%Y %H:%M:%S." (Date.fromTimeLocal time) ^ millis
+  end
+
 fun process_line str tstate =
   let
     fun process tstate (#"R", [t]) = gettm t tstate |>> refl |-> setth
@@ -416,7 +424,7 @@
           gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm
       | process (thy, state) (#"+", [s]) =
           let
-            val _ = tracing ("Noting: " ^ s)
+            val _ = tracing ("NOTING " ^ log_timestamp () ^ ": " ^ s)
           in
             (store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state)
           end