isabelle: src/Doc/Tutorial/ToyList/ToyList_Test.thy@05313b45a5ae (annotated)

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

author	wenzelm
	Tue, 10 Sep 2013 11:57:53 +0200
changeset 53498	05313b45a5ae
parent 53376	1d4a46f1fced
child 56208	06cc31dff138
permissions	-rw-r--r--