| author | wenzelm |
| Fri, 14 Mar 2014 15:26:52 +0100 | |
| changeset 56145 | a200bffe4027 |
| parent 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