--- 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.
--- 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.
--- 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}
*}
--- 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}%