--- a/NEWS Mon Oct 25 11:01:00 2010 +0200
+++ b/NEWS Mon Oct 25 11:16:23 2010 +0200
@@ -314,6 +314,10 @@
*** ML ***
+* Antiquotation @{assert} inlines a function bool -> unit that raises
+Fail if the argument is false. Due to inlining the source position of
+failed assertions is included in the error output.
+
* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
meaning.
--- a/doc-src/IsarImplementation/Thy/Base.thy Mon Oct 25 11:01:00 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Base.thy Mon Oct 25 11:16:23 2010 +0200
@@ -3,10 +3,4 @@
uses "../../antiquote_setup.ML"
begin
-(* FIXME move to src/Pure/ML/ml_antiquote.ML *)
-ML {*
- ML_Antiquote.inline "assert"
- (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")")
-*}
-
end
--- a/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 25 11:01:00 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 25 11:16:23 2010 +0200
@@ -1207,10 +1207,10 @@
\begin{description}
- \item @{text "@{assert}"} inlines a function @{text "bool \<Rightarrow> unit"}
- that raises @{ML Fail} if the argument is @{ML false}. Due to
- inlining the source position of failed assertions is included in the
- error output.
+ \item @{text "@{assert}"} inlines a function
+ @{ML_type "bool -> unit"} that raises @{ML Fail} if the argument is
+ @{ML false}. Due to inlining the source position of failed
+ assertions is included in the error output.
\end{description}
*}
--- a/doc-src/IsarImplementation/Thy/document/Base.tex Mon Oct 25 11:01:00 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Base.tex Mon Oct 25 11:16:23 2010 +0200
@@ -11,41 +11,8 @@
\ Base\isanewline
\isakeyword{imports}\ Main\isanewline
\isakeyword{uses}\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isacharslash}{\isachardot}{\isachardot}{\isacharslash}antiquote{\isacharunderscore}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-\isanewline
-%
-\isadelimML
+\isakeyword{begin}\isanewline
\isanewline
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\isanewline
-\ \ ML{\isacharunderscore}Antiquote{\isachardot}inline\ {\isachardoublequote}assert{\isachardoublequote}\isanewline
-\ \ \ \ {\isacharparenleft}Scan{\isachardot}succeed\ {\isachardoublequote}{\isacharparenleft}fn\ b\ {\isacharequal}{\isachargreater}\ if\ b\ then\ {\isacharparenleft}{\isacharparenright}\ else\ raise\ General{\isachardot}Fail\ {\isacharbackslash}{\isachardoublequote}Assertion\ failed{\isacharbackslash}{\isachardoublequote}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline
-{\isacharverbatimclose}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-\isanewline
-%
-\endisadelimML
-%
-\isadelimtheory
-\isanewline
-%
-\endisadelimtheory
-%
-\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Mon Oct 25 11:01:00 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Mon Oct 25 11:16:23 2010 +0200
@@ -1539,10 +1539,10 @@
\begin{description}
- \item \isa{{\isacharat}{\isacharbraceleft}assert{\isacharbraceright}} inlines a function \isa{bool\ {\isasymRightarrow}\ unit}
- that raises \verb|Fail| if the argument is \verb|false|. Due to
- inlining the source position of failed assertions is included in the
- error output.
+ \item \isa{{\isacharat}{\isacharbraceleft}assert{\isacharbraceright}} inlines a function
+ \verb|bool -> unit| that raises \verb|Fail| if the argument is
+ \verb|false|. Due to inlining the source position of failed
+ assertions is included in the error output.
\end{description}%
\end{isamarkuptext}%
--- a/src/Pure/ML/ml_antiquote.ML Mon Oct 25 11:01:00 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Mon Oct 25 11:16:23 2010 +0200
@@ -57,6 +57,9 @@
(** misc antiquotations **)
+val _ = inline "assert"
+ (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")");
+
val _ = inline "make_string" (Scan.succeed ml_make_string);
val _ = value "binding"