adapted to Poly/ML repository version 2e40cadc975a;
authorwenzelm
Fri Apr 01 11:45:04 2016 +0200 (2016-04-01)
changeset 627840371c369ab1d
parent 62783 75ee05386b90
child 62785 70b9c7d4ed7f
adapted to Poly/ML repository version 2e40cadc975a;
src/Pure/General/pretty.ML
src/Pure/ML/ml_pretty.ML
     1.1 --- a/src/Pure/General/pretty.ML	Thu Mar 31 23:36:33 2016 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Fri Apr 01 11:45:04 2016 +0200
     1.3 @@ -74,7 +74,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: int -> T -> ML_Pretty.pretty
     1.8 +  val to_ML: FixedInt.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
     2.1 --- a/src/Pure/ML/ml_pretty.ML	Thu Mar 31 23:36:33 2016 +0200
     2.2 +++ b/src/Pure/ML/ml_pretty.ML	Fri Apr 01 11:45:04 2016 +0200
     2.3 @@ -13,8 +13,10 @@
     2.4    val block: pretty list -> pretty
     2.5    val str: string -> pretty
     2.6    val brk: FixedInt.int -> pretty
     2.7 -  val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
     2.8 -  val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
     2.9 +  val pair: ('a * FixedInt.int -> pretty) -> ('b * FixedInt.int -> pretty) ->
    2.10 +    ('a * 'b) * FixedInt.int -> pretty
    2.11 +  val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) ->
    2.12 +    'a list * FixedInt.int -> pretty
    2.13    val to_polyml: pretty -> PolyML.pretty
    2.14    val from_polyml: PolyML.pretty -> pretty
    2.15    val get_print_depth: unit -> int