1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Debug.thy	Sun Jul 22 09:56:34 2012 +0200
     1.3 @@ -0,0 +1,40 @@
     1.4 +(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +
     1.6 +header {* Debugging facilities for code generated towards Isabelle/ML *}
     1.7 +
     1.8 +theory Debug
     1.9 +imports Main
    1.10 +begin
    1.11 +
    1.12 +definition trace :: "String.literal \<Rightarrow> unit" where
    1.13 +  [simp]: "trace s = ()"
    1.14 +
    1.15 +definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.16 +  [simp]: "tracing s = id"
    1.17 +
    1.18 +lemma [code]:
    1.19 +  "tracing s = (let u = trace s in id)"
    1.20 +  by simp
    1.21 +
    1.22 +definition flush :: "'a \<Rightarrow> unit" where
    1.23 +  [simp]: "flush x = ()"
    1.24 +
    1.25 +definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
    1.26 +  [simp]: "flushing x = id"
    1.27 +
    1.28 +lemma [code, code_unfold]:
    1.29 +  "flushing x = (let u = flush x in id)"
    1.30 +  by simp
    1.31 +
    1.32 +definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.33 +  [simp]: "timing s f x = f x"
    1.34 +
    1.35 +code_const trace and flush and timing
    1.36 +  (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg")
    1.37 +
    1.38 +code_reserved Eval Output PolyML Timing
    1.39 +
    1.40 +hide_const (open) trace tracing flush flushing timing
    1.41 +
    1.42 +end
    1.43 +