| changeset 53376 | 1d4a46f1fced |
| child 56208 | 06cc31dff138 |
| 53375:78693e46a237 | 53376:1d4a46f1fced |
|---|---|
1 theory ToyList_Test |
|
2 imports Datatype |
|
3 begin |
|
4 |
|
5 ML {* (* FIXME somewhat non-standard, fragile *) |
|
6 let |
|
7 val texts = |
|
8 map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode) |
|
9 ["ToyList1", "ToyList2"]; |
|
10 val trs = Outer_Syntax.parse Position.start (implode texts); |
|
11 val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel; |
|
12 in @{assert} (Toplevel.is_toplevel end_state) end; |
|
13 *} |
|
14 |
|
15 end |
|
16 |