--- a/src/Pure/ML-Systems/ml_pretty.ML Sat Mar 21 15:09:44 2009 +0100
+++ b/src/Pure/ML-Systems/ml_pretty.ML Sat Mar 21 19:58:44 2009 +0100
@@ -1,22 +1,16 @@
(* Title: Pure/ML-Systems/ml_pretty.ML
Author: Makarius
-Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in
-Poly/ML 5.3).
+Raw datatype for ML pretty printing.
*)
structure ML_Pretty =
struct
-datatype context =
- ContextLocation of
- {file: string, startLine: int, startPosition: int, endLine: int, endPosition: int} |
- ContextParentStructure of string * context list;
-
datatype pretty =
- PrettyBlock of int * bool * context list * pretty list |
- PrettyBreak of int * int |
- PrettyString of string;
+ Block of (string * string) * pretty list * int |
+ String of string * int |
+ Break of bool * int;
end;