# HG changeset patch
# User haftmann
# Date 1243333861 -7200
# Node ID 03a35fbc9dc6f523d17e23724fa51764c8b3cfa9
# Parent  d54dc8956d486f67459e29c22f47a171e74509fc
documented print_codeproc command

diff -r d54dc8956d48 -r 03a35fbc9dc6 doc-src/Codegen/Thy/Program.thy
--- a/doc-src/Codegen/Thy/Program.thy	Mon May 25 22:14:59 2009 -0700
+++ b/doc-src/Codegen/Thy/Program.thy	Tue May 26 12:31:01 2009 +0200
@@ -204,7 +204,7 @@
   interface.
 
   \noindent The current setup of the preprocessor may be inspected using
-  the @{command print_codesetup} command.
+  the @{command print_codeproc} command.
   @{command code_thms} provides a convenient
   mechanism to inspect the impact of a preprocessor setup
   on code equations.
diff -r d54dc8956d48 -r 03a35fbc9dc6 doc-src/Codegen/Thy/document/Program.tex
--- a/doc-src/Codegen/Thy/document/Program.tex	Mon May 25 22:14:59 2009 -0700
+++ b/doc-src/Codegen/Thy/document/Program.tex	Tue May 26 12:31:01 2009 +0200
@@ -486,7 +486,7 @@
   interface.
 
   \noindent The current setup of the preprocessor may be inspected using
-  the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+  the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
   \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
   mechanism to inspect the impact of a preprocessor setup
   on code equations.
diff -r d54dc8956d48 -r 03a35fbc9dc6 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 25 22:14:59 2009 -0700
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue May 26 12:31:01 2009 +0200
@@ -1065,6 +1065,7 @@
     @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+    @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{attribute_def (HOL) code} & : & @{text attribute} \\
   \end{matharray}
 
@@ -1228,8 +1229,10 @@
   preprocessing.
 
   \item @{command (HOL) "print_codesetup"} gives an overview on
-  selected code equations, code generator datatypes and
-  preprocessor setup.
+  selected code equations and code generator datatypes.
+
+  \item @{command (HOL) "print_codeproc"} prints the setup
+  of the code generator preprocessor.
 
   \end{description}
 *}
diff -r d54dc8956d48 -r 03a35fbc9dc6 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 25 22:14:59 2009 -0700
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue May 26 12:31:01 2009 +0200
@@ -1074,6 +1074,7 @@
     \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
+    \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
   \end{matharray}
 
@@ -1234,8 +1235,10 @@
   preprocessing.
 
   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
-  selected code equations, code generator datatypes and
-  preprocessor setup.
+  selected code equations and code generator datatypes.
+
+  \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
+  of the code generator preprocessor.
 
   \end{description}%
 \end{isamarkuptext}%