isabelle: src/Pure/ML-Systems/install_pp_polyml-5.3.ML@08a39a957ed7 (annotated)

31433 12f5f6af3d2d less experimental polyml-5.3; wenzelm parents: 31318 diff changeset	1	(* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML
30633 cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3; wenzelm parents: diff changeset	2
31433 12f5f6af3d2d less experimental polyml-5.3; wenzelm parents: 31318 diff changeset	3	Extra toplevel pretty-printing for Poly/ML 5.3.
30633 cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3; wenzelm parents: diff changeset	4	*)
cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3; wenzelm parents: diff changeset	5
31318 133d1cfd6ae7 explicit PolyML qualification; wenzelm parents: 31311 diff changeset	6	PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
30633 cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3; wenzelm parents: diff changeset	7	(case Future.peek x of
31318 133d1cfd6ae7 explicit PolyML qualification; wenzelm parents: 31311 diff changeset	8	NONE => PolyML.PrettyString "<future>"
133d1cfd6ae7 explicit PolyML qualification; wenzelm parents: 31311 diff changeset	9	\| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
30714 88bc86d7dec3 simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally; wenzelm parents: 30633 diff changeset	10	\| SOME (Exn.Result y) => pretty (y, depth)));
30633 cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3; wenzelm parents: diff changeset	11
31318 133d1cfd6ae7 explicit PolyML qualification; wenzelm parents: 31311 diff changeset	12	PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
30633 cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3; wenzelm parents: diff changeset	13	(case Lazy.peek x of
31318 133d1cfd6ae7 explicit PolyML qualification; wenzelm parents: 31311 diff changeset	14	NONE => PolyML.PrettyString "<lazy>"
133d1cfd6ae7 explicit PolyML qualification; wenzelm parents: 31311 diff changeset	15	\| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
30714 88bc86d7dec3 simplified addPrettyPrinter setup: may pass (fn ...) directly if type constraints are omitted -- addPrettyPrinter treated as a special case internally; wenzelm parents: 30633 diff changeset	16	\| SOME (Exn.Result y) => pretty (y, depth)));
30633 cc18ae3c1c7f extra toplevel pretty-printing for Poly/ML; experimental version for Poly/ML 5.3; wenzelm parents: diff changeset	17

author	blanchet
	Thu, 22 Oct 2009 14:51:47 +0200
changeset 33192	08a39a957ed7
parent 31433	12f5f6af3d2d
child 33538	edf497b5b5d2
permissions	-rw-r--r--