Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/ML-Systems/install_pp_polyml-5.3.ML
author wenzelm
Sat, 06 Jun 2009 19:58:10 +0200
changeset 31471 e3987b32e401
parent 31433 12f5f6af3d2d
child 33538 edf497b5b5d2
permissions -rw-r--r--
use_text: pass file name to compiler, tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
















isabelle