equal
deleted
inserted
replaced
|
1 (* Title: Pure/ML-Systems/ml_pretty.ML |
|
2 Author: Makarius |
|
3 |
|
4 Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in |
|
5 Poly/ML 5.3). |
|
6 *) |
|
7 |
|
8 structure ML_Pretty = |
|
9 struct |
|
10 |
|
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 = |
|
17 PrettyBlock of int * bool * context list * pretty list | |
|
18 PrettyBreak of int * int | |
|
19 PrettyString of string; |
|
20 |
|
21 end; |
|
22 |