# HG changeset patch
# User wenzelm
# Date 1287998183 -7200
# Node ID 93e7935d4cb52c819461286e1a35fdc4bd0802fe
# Parent  ebe2253e5c0ea8277643e7a67d601f8d79a889b1
added ML antiquotation @{assert};

diff -r ebe2253e5c0e -r 93e7935d4cb5 NEWS
--- 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.
 
diff -r ebe2253e5c0e -r 93e7935d4cb5 doc-src/IsarImplementation/Thy/Base.thy
--- 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
diff -r ebe2253e5c0e -r 93e7935d4cb5 doc-src/IsarImplementation/Thy/ML.thy
--- 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}
 *}
diff -r ebe2253e5c0e -r 93e7935d4cb5 doc-src/IsarImplementation/Thy/document/Base.tex
--- 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
diff -r ebe2253e5c0e -r 93e7935d4cb5 doc-src/IsarImplementation/Thy/document/ML.tex
--- 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}%
diff -r ebe2253e5c0e -r 93e7935d4cb5 src/Pure/ML/ml_antiquote.ML
--- 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"