# HG changeset patch
# User wenzelm
# Date 1287425167 -3600
# Node ID 5ec01d5acd0ce5e104d70c74377259d778fe352f
# Parent  a724b90f951ef8ea6b207f76843084fa56bb6aef
more robust examples: explicit @{assert} instead of unchecked output;

diff -r a724b90f951e -r 5ec01d5acd0c doc-src/IsarImplementation/Thy/Base.thy
--- a/doc-src/IsarImplementation/Thy/Base.thy	Mon Oct 18 16:23:55 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Base.thy	Mon Oct 18 19:06:07 2010 +0100
@@ -3,4 +3,10 @@
 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 a724b90f951e -r 5ec01d5acd0c doc-src/IsarImplementation/Thy/Isar.thy
--- a/doc-src/IsarImplementation/Thy/Isar.thy	Mon Oct 18 16:23:55 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy	Mon Oct 18 19:06:07 2010 +0100
@@ -164,7 +164,10 @@
 
 example_proof
   have A and B and C
-    ML_val {* Thm.nprems_of (#goal @{Isar.goal}) *}
+    ML_val {*
+      val n = Thm.nprems_of (#goal @{Isar.goal});
+      @{assert} (n = 3);
+    *}
     oops
 
 text {* Here we see 3 individual subgoals in the same way as regular
diff -r a724b90f951e -r 5ec01d5acd0c doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Mon Oct 18 16:23:55 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Mon Oct 18 19:06:07 2010 +0100
@@ -470,6 +470,21 @@
   \end{description}
 *}
 
+text %mlantiq {*
+  \begin{matharray}{rcl}
+  @{ML_antiquotation_def "assert"} & : & @{text ML_antiquotation} \\
+  \end{matharray}
+
+  \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.
+
+  \end{description}
+*}
+
 
 section {* Basic data types *}
 
@@ -648,7 +663,10 @@
   val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
 
   val list1 = fold cons items [];
+  @{assert} (list1 = rev items);
+
   val list2 = fold_rev cons items [];
+  @{assert} (list2 = items);
 *}
 
 
diff -r a724b90f951e -r 5ec01d5acd0c doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Oct 18 16:23:55 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Oct 18 19:06:07 2010 +0100
@@ -643,19 +643,20 @@
   declarations, while we can retrieve the current value from the
   context via @{ML Config.get}.  *}
 
-ML_val {* Config.get @{context} my_flag *}
+ML_val {* @{assert} (Config.get @{context} my_flag = false) *}
 
 declare [[my_flag = true]]
 
-ML_val {* Config.get @{context} my_flag *}
+ML_val {* @{assert} (Config.get @{context} my_flag = true) *}
 
 example_proof
-  note [[my_flag = false]]
-  ML_val {* Config.get @{context} my_flag *}
+  {
+    note [[my_flag = false]]
+    ML_val {* @{assert} (Config.get @{context} my_flag = false) *}
+  }
+  ML_val {* @{assert} (Config.get @{context} my_flag = true) *}
 qed
 
-ML_val {* Config.get @{context} my_flag *}
-
 
 section {* Names \label{sec:names} *}
 
@@ -888,8 +889,12 @@
   fresh names from the initial @{ML Name.context}. *}
 
 ML {*
-  Name.invents Name.context "a" 5;
-  #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] Name.context);
+  val list1 = Name.invents Name.context "a" 5;
+  @{assert} (list1 = ["a", "b", "c", "d", "e"]);
+
+  val list2 =
+    #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] Name.context);
+  @{assert} (list2 = ["x", "xa", "a", "aa", "'a", "'aa"]);
 *}
 
 text {* \medskip The same works reletively to the formal context as
@@ -900,8 +905,13 @@
 
 ML {*
   val names = Variable.names_of @{context};
-  Name.invents names "a" 5;
-  #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] names);
+
+  val list1 = Name.invents names "a" 5;
+  @{assert} (list1 = ["d", "e", "f", "g", "h"]);
+
+  val list2 =
+    #1 (Name.variants ["x", "x", "a", "a", "'a", "'a"] names);
+  @{assert} (list2 = ["x", "xa", "aa", "ab", "'aa", "'ab"]);
 *}
 
 end