isabelle: src/Doc/Tutorial/ToyList/ToyList_Test.thy@3a1b1bda702f (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 =
56208 06cc31dff138 clarifed module name; wenzelm parents: 53376 diff changeset	8	map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
57083 5c26000e1042 more portable file names; wenzelm parents: 56208 diff changeset	9	["ToyList1.txt", "ToyList2.txt"];
53376 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
	Mon, 21 Jul 2014 20:36:25 +0200
changeset 57596	3a1b1bda702f
parent 57083	5c26000e1042
child 57626	2288a6f17930
permissions	-rw-r--r--