# 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 \ theory"} \\ @{command_def (HOL) "code_abort"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{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}%