documented print_codeproc command
authorhaftmann
Tue May 26 12:31:01 2009 +0200 (2009-05-26)
changeset 3125403a35fbc9dc6
parent 31253 d54dc8956d48
child 31255 0f8cb37bcafd
documented print_codeproc command
doc-src/Codegen/Thy/Program.thy
doc-src/Codegen/Thy/document/Program.tex
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     1.1 --- a/doc-src/Codegen/Thy/Program.thy	Mon May 25 22:14:59 2009 -0700
     1.2 +++ b/doc-src/Codegen/Thy/Program.thy	Tue May 26 12:31:01 2009 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4    interface.
     1.5  
     1.6    \noindent The current setup of the preprocessor may be inspected using
     1.7 -  the @{command print_codesetup} command.
     1.8 +  the @{command print_codeproc} command.
     1.9    @{command code_thms} provides a convenient
    1.10    mechanism to inspect the impact of a preprocessor setup
    1.11    on code equations.
     2.1 --- a/doc-src/Codegen/Thy/document/Program.tex	Mon May 25 22:14:59 2009 -0700
     2.2 +++ b/doc-src/Codegen/Thy/document/Program.tex	Tue May 26 12:31:01 2009 +0200
     2.3 @@ -486,7 +486,7 @@
     2.4    interface.
     2.5  
     2.6    \noindent The current setup of the preprocessor may be inspected using
     2.7 -  the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
     2.8 +  the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
     2.9    \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
    2.10    mechanism to inspect the impact of a preprocessor setup
    2.11    on code equations.
     3.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 25 22:14:59 2009 -0700
     3.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue May 26 12:31:01 2009 +0200
     3.3 @@ -1065,6 +1065,7 @@
     3.4      @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
     3.5      @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
     3.6      @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     3.7 +    @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     3.8      @{attribute_def (HOL) code} & : & @{text attribute} \\
     3.9    \end{matharray}
    3.10  
    3.11 @@ -1228,8 +1229,10 @@
    3.12    preprocessing.
    3.13  
    3.14    \item @{command (HOL) "print_codesetup"} gives an overview on
    3.15 -  selected code equations, code generator datatypes and
    3.16 -  preprocessor setup.
    3.17 +  selected code equations and code generator datatypes.
    3.18 +
    3.19 +  \item @{command (HOL) "print_codeproc"} prints the setup
    3.20 +  of the code generator preprocessor.
    3.21  
    3.22    \end{description}
    3.23  *}
     4.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 25 22:14:59 2009 -0700
     4.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue May 26 12:31:01 2009 +0200
     4.3 @@ -1074,6 +1074,7 @@
     4.4      \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}} \\
     4.5      \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}} \\
     4.6      \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}} \\
     4.7 +    \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}} \\
     4.8      \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
     4.9    \end{matharray}
    4.10  
    4.11 @@ -1234,8 +1235,10 @@
    4.12    preprocessing.
    4.13  
    4.14    \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
    4.15 -  selected code equations, code generator datatypes and
    4.16 -  preprocessor setup.
    4.17 +  selected code equations and code generator datatypes.
    4.18 +
    4.19 +  \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
    4.20 +  of the code generator preprocessor.
    4.21  
    4.22    \end{description}%
    4.23  \end{isamarkuptext}%