src/Pure/ML-Systems/install_pp_polyml.ML
author wenzelm
Sun, 31 May 2009 14:51:21 +0200
changeset 31312 1c00e4ff3c99
parent 29564 f8b933a62151
child 31314 b58d6a33b57f
permissions -rw-r--r--
more modular setup of runtime compilation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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