| author | wenzelm |
| Wed, 02 Apr 2014 11:55:37 +0200 | |
| changeset 56358 | ed09e5f3aedf |
| parent 56208 | 06cc31dff138 |
| child 57083 | 5c26000e1042 |
| 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", "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