author | wenzelm |
Sat, 24 May 2014 20:07:26 +0200 | |
changeset 57083 | 5c26000e1042 |
parent 56208 | 06cc31dff138 |
child 57626 | 2288a6f17930 |
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 (Resources.master_directory @{theory}) o Path.explode) ["ToyList1.txt", "ToyList2.txt"]; 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