author | wenzelm |
Tue, 03 Sep 2013 11:55:59 +0200 | |
changeset 53376 | 1d4a46f1fced |
child 56208 | 06cc31dff138 |
permissions | -rw-r--r-- |
theory ToyList_Test imports Datatype begin 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); val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel; in @{assert} (Toplevel.is_toplevel end_state) end; *} end