author  wenzelm 
Sat, 21 Mar 2009 20:38:49 +0100  
changeset 30633  cc18ae3c1c7f 
child 30714  88bc86d7dec3 
permissions  rwrr 
30633
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/MLSystems/install_pp_polymlexperimental.ML 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

2 

cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

3 
Extra toplevel prettyprinting for Poly/ML; experimental version for 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

4 
Poly/ML 5.3. 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

5 
*) 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

6 

cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

7 
local 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

8 

cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

9 
fun pretty_future depth (pretty: 'a * int > pretty) (x: 'a future) = 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

10 
(case Future.peek x of 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

11 
NONE => PrettyString "<future>" 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

12 
 SOME (Exn.Exn _) => PrettyString "<failed>" 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

13 
 SOME (Exn.Result y) => pretty (y, depth)); 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

14 

cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

15 
fun pretty_lazy depth (pretty: 'a * int > pretty) (x: 'a lazy) = 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

16 
(case Lazy.peek x of 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

17 
NONE => PrettyString "<lazy>" 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

18 
 SOME (Exn.Exn _) => PrettyString "<failed>" 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

19 
 SOME (Exn.Result y) => pretty (y, depth)); 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

20 

cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

21 
in 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

22 

cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

23 
val _ = addPrettyPrinter pretty_future; 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

24 
val _ = addPrettyPrinter pretty_lazy; 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

25 

cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

26 
end; 
cc18ae3c1c7f
extra toplevel prettyprinting for Poly/ML; experimental version for Poly/ML 5.3;
wenzelm
parents:
diff
changeset

27 