--- a/doc-src/Codegen/Thy/Foundations.thy Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Wed Oct 19 23:07:48 2011 +0200
@@ -125,12 +125,6 @@
code_thms} (see \secref{sec:equations}) provides a convenient
mechanism to inspect the impact of a preprocessor setup on code
equations.
-
- \begin{warn}
- Attribute @{attribute code_unfold} also applies to the
- preprocessor of the ancient @{text "SML code generator"}; in case
- this is not what you intend, use @{attribute code_inline} instead.
- \end{warn}
*}
--- a/doc-src/Codegen/Thy/Introduction.thy Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Wed Oct 19 23:07:48 2011 +0200
@@ -236,15 +236,6 @@
\begin{center}\textit{Happy proving, happy hacking!}\end{center}
\end{minipage}}}\end{center}
-
- \begin{warn}
- There is also a more ancient code generator in Isabelle by Stefan
- Berghofer \cite{Berghofer-Nipkow:2002}. Although its
- functionality is covered by the code generator presented here, it
- will sometimes show up as an artifact. In case of ambiguity, we
- will refer to the framework described here as @{text "generic code
- generator"}, to the other as @{text "SML code generator"}.
- \end{warn}
*}
end
--- a/doc-src/Codegen/Thy/document/Foundations.tex Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Wed Oct 19 23:07:48 2011 +0200
@@ -184,13 +184,7 @@
\noindent The current setup of the preprocessor may be inspected
using the \indexdef{}{command}{print\_codeproc}\hypertarget{command.print-codeproc}{\hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}}} command. \indexdef{}{command}{code\_thms}\hypertarget{command.code-thms}{\hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}} (see \secref{sec:equations}) provides a convenient
mechanism to inspect the impact of a preprocessor setup on code
- equations.
-
- \begin{warn}
- Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}unfold}}} also applies to the
- preprocessor of the ancient \isa{SML\ code\ generator}; in case
- this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}} instead.
- \end{warn}%
+ equations.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Oct 19 22:54:26 2011 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Oct 19 23:07:48 2011 +0200
@@ -560,15 +560,7 @@
\begin{center}\textit{Happy proving, happy hacking!}\end{center}
- \end{minipage}}}\end{center}
-
- \begin{warn}
- There is also a more ancient code generator in Isabelle by Stefan
- Berghofer \cite{Berghofer-Nipkow:2002}. Although its
- functionality is covered by the code generator presented here, it
- will sometimes show up as an artifact. In case of ambiguity, we
- will refer to the framework described here as \isa{generic\ code\ generator}, to the other as \isa{SML\ code\ generator}.
- \end{warn}%
+ \end{minipage}}}\end{center}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/src/Pure/Isar/code.ML Wed Oct 19 22:54:26 2011 +0200
+++ b/src/Pure/Isar/code.ML Wed Oct 19 23:07:48 2011 +0200
@@ -76,9 +76,6 @@
val get_case_cong: theory -> string -> thm option
val undefineds: theory -> string list
val print_codesetup: theory -> unit
-
- (*infrastructure*)
- val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
end;
signature CODE_DATA_ARGS =
@@ -1264,26 +1261,6 @@
end;
-(** infrastructure **)
-
-(* cf. src/HOL/Tools/recfun_codegen.ML *)
-
-structure Code_Target_Attr = Theory_Data
-(
- type T = (string -> thm -> theory -> theory) option;
- val empty = NONE;
- val extend = I;
- val merge = merge_options;
-);
-
-fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
-
-fun code_target_attr prefix thm thy =
- let
- val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
- in thy |> add_warning_eqn thm |> attr prefix thm end;
-
-
(* setup *)
val _ = Context.>> (Context.map_theory
@@ -1294,8 +1271,6 @@
|| Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
|| Args.$$$ "abstype" |-- Scan.succeed (mk_attribute add_abstype)
|| Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
- || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
- (mk_attribute o code_target_attr))
|| Scan.succeed (mk_attribute add_warning_eqn);
in
Datatype_Interpretation.init