src/HOL/Code_Evaluation.thy
changeset 33473 3b275a0bf18c
parent 32740 9dd0a2f83429
child 33553 35f2b30593a8
     1.1 --- a/src/HOL/Code_Evaluation.thy	Thu Nov 05 14:47:27 2009 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Nov 06 08:11:58 2009 +0100
     1.3 @@ -243,6 +243,26 @@
     1.4  hide const dummy_term App valapp
     1.5  hide (open) const Const termify valtermify term_of term_of_num
     1.6  
     1.7 +subsection {* Tracing of generated and evaluated code *}
     1.8 +
     1.9 +definition tracing :: "String.literal => 'a => 'a"
    1.10 +where
    1.11 +  [code del]: "tracing s x = x"
    1.12 +
    1.13 +ML {*
    1.14 +structure Code_Evaluation =
    1.15 +struct
    1.16 +
    1.17 +fun tracing s x = (Output.tracing s; x)
    1.18 +
    1.19 +end
    1.20 +*}
    1.21 +
    1.22 +code_const "tracing :: String.literal => 'a => 'a"
    1.23 +  (Eval "Code'_Evaluation.tracing")
    1.24 +
    1.25 +hide (open) const tracing
    1.26 +code_reserved Eval Code_Evaluation
    1.27  
    1.28  subsection {* Evaluation setup *}
    1.29