| author | blanchet |
| Fri, 30 May 2014 12:27:51 +0200 | |
| changeset 57121 | 426ab5fabcae |
| parent 57083 | 5c26000e1042 |
| 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