observe ML print depth;
authorwenzelm
Fri Mar 18 21:29:10 2016 +0100 (2016-03-18)
changeset 62673b5c57430b9dd
parent 62672 068b430e678f
child 62674 6cfa0de8bb99
observe ML print depth;
src/Pure/ML/ml_pp.ML
     1.1 --- a/src/Pure/ML/ml_pp.ML	Fri Mar 18 21:21:09 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_pp.ML	Fri Mar 18 21:29:10 2016 +0100
     1.3 @@ -8,24 +8,23 @@
     1.4  struct
     1.5  
     1.6  val _ =
     1.7 -  PolyML.addPrettyPrinter
     1.8 -    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
     1.9 +  PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
    1.10  
    1.11  val _ =
    1.12 -  PolyML.addPrettyPrinter
    1.13 -    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_thm Thy_Info.pure_theory);
    1.14 +  PolyML.addPrettyPrinter (fn depth => fn _ =>
    1.15 +    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
    1.16  
    1.17  val _ =
    1.18 -  PolyML.addPrettyPrinter
    1.19 -    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_cterm Thy_Info.pure_theory);
    1.20 +  PolyML.addPrettyPrinter (fn depth => fn _ =>
    1.21 +    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
    1.22  
    1.23  val _ =
    1.24 -  PolyML.addPrettyPrinter
    1.25 -    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_ctyp Thy_Info.pure_theory);
    1.26 +  PolyML.addPrettyPrinter (fn depth => fn _ =>
    1.27 +    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
    1.28  
    1.29  val _ =
    1.30 -  PolyML.addPrettyPrinter
    1.31 -    (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_typ Thy_Info.pure_theory);
    1.32 +  PolyML.addPrettyPrinter (fn depth => fn _ =>
    1.33 +    ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
    1.34  
    1.35  
    1.36  local