# HG changeset patch
# User wenzelm
# Date 1361905871 -3600
# Node ID 8799eadf61fb668800e49b45bb351fbfb6ab081c
# Parent  44a521ff87cfb528870e4cc11b99753094162e0a
updated Toplevel.command_exception;

diff -r 44a521ff87cf -r 8799eadf61fb src/Doc/Tutorial/ToyList/ToyList.thy
--- 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;
 *}
 (*>*)