clarified Pretty.T toplevel pp;
authorwenzelm
Fri Mar 18 17:51:57 2016 +0100 (2016-03-18)
changeset 62667254582abf067
parent 62666 00aff1da05ae
child 62668 360d3464919c
clarified Pretty.T toplevel pp;
src/Pure/General/pretty.ML
src/Pure/ML/ml_pp.ML
     1.1 --- a/src/Pure/General/pretty.ML	Fri Mar 18 17:11:30 2016 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Fri Mar 18 17:51:57 2016 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4    val block_enclose: T * T -> T list -> T
     1.5    val writeln_chunks: T list -> unit
     1.6    val writeln_chunks2: T list -> unit
     1.7 -  val to_ML: T -> ML_Pretty.pretty
     1.8 +  val to_ML: int -> T -> ML_Pretty.pretty
     1.9    val from_ML: ML_Pretty.pretty -> T
    1.10    val to_polyml: T -> PolyML.pretty
    1.11    val from_polyml: PolyML.pretty -> T
    1.12 @@ -376,11 +376,12 @@
    1.13  
    1.14  (** toplevel pretty printing **)
    1.15  
    1.16 -fun to_ML (Block (m, consistent, indent, prts, _)) =
    1.17 -      ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map to_ML prts)
    1.18 -  | to_ML (Break (force, wd, ind)) =
    1.19 +fun to_ML 0 (Block _) = ML_Pretty.str "..."
    1.20 +  | to_ML depth (Block (m, consistent, indent, prts, _)) =
    1.21 +      ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map (to_ML (depth - 1)) prts)
    1.22 +  | to_ML _ (Break (force, wd, ind)) =
    1.23        ML_Pretty.Break (force, FixedInt.fromInt wd, FixedInt.fromInt ind)
    1.24 -  | to_ML (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
    1.25 +  | to_ML _ (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
    1.26  
    1.27  fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
    1.28        make_block m consistent (FixedInt.toInt indent) (map from_ML prts)
    1.29 @@ -388,12 +389,14 @@
    1.30        Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
    1.31    | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len);
    1.32  
    1.33 -val to_polyml = to_ML #> ML_Pretty.to_polyml;
    1.34 +val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
    1.35  val from_polyml = ML_Pretty.from_polyml #> from_ML;
    1.36  
    1.37  end;
    1.38  
    1.39 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => fn _: T => to_polyml (str "<pretty>"));
    1.40 +val _ =
    1.41 +  PolyML.addPrettyPrinter (fn depth => fn _ => ML_Pretty.to_polyml o to_ML (depth * 2 + 1) o quote);
    1.42 +
    1.43  val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
    1.44  
    1.45  end;
     2.1 --- a/src/Pure/ML/ml_pp.ML	Fri Mar 18 17:11:30 2016 +0100
     2.2 +++ b/src/Pure/ML/ml_pp.ML	Fri Mar 18 17:51:57 2016 +0100
     2.3 @@ -104,7 +104,7 @@
     2.4  
     2.5  val _ =
     2.6    PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
     2.7 -    ML_Pretty.to_polyml (Pretty.to_ML (prt_proof false depth prf)));
     2.8 +    ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
     2.9  
    2.10  end;
    2.11