isabelle: src/Pure/ML-Systems/install_pp_polyml.ML@7c871a9cf6f4 (annotated)

28557 6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML; wenzelm parents: diff changeset	1	(* Title: Pure/ML-Systems/install_pp_polyml.ML
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML; wenzelm parents: diff changeset	2
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML; wenzelm parents: diff changeset	3	Extra toplevel pretty-printing for Poly/ML.
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML; wenzelm parents: diff changeset	4	*)
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML; wenzelm parents: diff changeset	5
28975 ec120dc11e8b renamed type Lazy.T to lazy; wenzelm parents: 28673 diff changeset	6	install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
28557 6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML; wenzelm parents: diff changeset	7	(case Future.peek x of
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML; wenzelm parents: diff changeset	8	NONE => str "<future>"
28570 81d97311c057 tuned output; wenzelm parents: 28557 diff changeset	9	\| SOME (Exn.Exn _) => str "<failed>"
28557 6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML; wenzelm parents: diff changeset	10	\| SOME (Exn.Result y) => print (y, depth)));
6a661aeff564 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML; wenzelm parents: diff changeset	11
28975 ec120dc11e8b renamed type Lazy.T to lazy; wenzelm parents: 28673 diff changeset	12	install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
28673 d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy; wenzelm parents: 28672 diff changeset	13	(case Lazy.peek x of
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy; wenzelm parents: 28672 diff changeset	14	NONE => str "<lazy>"
28672 0baf1d9c6780 adapted Susp.peek; wenzelm parents: 28570 diff changeset	15	\| SOME (Exn.Exn _) => str "<failed>"
0baf1d9c6780 adapted Susp.peek; wenzelm parents: 28570 diff changeset	16	\| SOME (Exn.Result y) => print (y, depth)));
0baf1d9c6780 adapted Susp.peek; wenzelm parents: 28570 diff changeset	17

author	huffman
	Mon, 27 Apr 2009 07:26:17 -0700
changeset 31007	7c871a9cf6f4
parent 29564	f8b933a62151
child 31314	b58d6a33b57f
permissions	-rw-r--r--