# HG changeset patch
# User haftmann
# Date 1649497242 -7200
# Node ID e0fa345f1aab0b34c625a0a713deedded5a1d2a3
# Parent  7b75a2c5b142f3cf407a6e0b1eecf08b25561773
documentation on diagnostic devices for code generation

diff -r 7b75a2c5b142 -r e0fa345f1aab src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Apr 09 11:27:09 2022 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Apr 09 11:40:42 2022 +0200
@@ -2282,7 +2282,10 @@
     @{command_def (HOL) "code_identifier"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def (HOL) "code_monad"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def (HOL) "code_reflect"} & : & \<open>theory \<rightarrow> theory\<close> \\
-    @{command_def (HOL) "code_pred"} & : & \<open>theory \<rightarrow> proof(prove)\<close>
+    @{command_def (HOL) "code_pred"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
+    @{attribute_def (HOL) code_timing} & : & \<open>attribute\<close> \\
+    @{attribute_def (HOL) code_simp_trace} & : & \<open>attribute\<close> \\
+    @{attribute_def (HOL) code_runtime_trace} & : & \<open>attribute\<close>
   \end{matharray}
 
   \<^rail>\<open>
@@ -2501,6 +2504,15 @@
   a set of introduction rules. Optional mode annotations determine which
   arguments are supposed to be input or output. If alternative introduction
   rules are declared, one must prove a corresponding elimination rule.
+
+  \<^descr> @{attribute (HOL) "code_timing"} scrapes timing samples from different
+  stages of the code generator.
+
+  \<^descr> @{attribute (HOL) "code_simp_trace"} traces the simplifier when it is
+  used with code equations.
+
+  \<^descr> @{attribute (HOL) "code_runtime_trace"} traces ML code generated
+  dynamically for execution.
 \<close>
 
 end