--- a/src/Doc/Tutorial/ToyList/ToyList.thy Tue Feb 26 20:09:25 2013 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Tue Feb 26 20:11:11 2013 +0100
@@ -3,13 +3,14 @@
begin
(*<*)
-ML {*
+ML {* (* FIXME somewhat non-standard, fragile *)
let
val texts =
map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode)
["ToyList1", "ToyList2"];
val trs = Outer_Syntax.parse Position.start (implode texts);
- in @{assert} (Toplevel.is_toplevel (fold Toplevel.command trs Toplevel.toplevel)) end;
+ val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
+ in @{assert} (Toplevel.is_toplevel end_state) end;
*}
(*>*)