src/Pure/ML-Systems/ml_pretty.ML
changeset 30623 9ed1122d6cd2
parent 30622 dba663f1afa8
child 38635 f76ad0771f67
equal deleted inserted replaced
30622:dba663f1afa8 30623:9ed1122d6cd2
     1 (*  Title:      Pure/ML-Systems/ml_pretty.ML
     1 (*  Title:      Pure/ML-Systems/ml_pretty.ML
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in
     4 Raw datatype for ML pretty printing.
     5 Poly/ML 5.3).
       
     6 *)
     5 *)
     7 
     6 
     8 structure ML_Pretty =
     7 structure ML_Pretty =
     9 struct
     8 struct
    10 
     9 
    11 datatype context =
       
    12   ContextLocation of
       
    13     {file: string, startLine: int, startPosition: int, endLine: int, endPosition: int} |
       
    14   ContextParentStructure of string * context list;
       
    15 
       
    16 datatype pretty =
    10 datatype pretty =
    17   PrettyBlock of int * bool * context list * pretty list |
    11   Block of (string * string) * pretty list * int |
    18   PrettyBreak of int * int |
    12   String of string * int |
    19   PrettyString of string;
    13   Break of bool * int;
    20 
    14 
    21 end;
    15 end;
    22 
    16