# HG changeset patch
# User wenzelm
# Date 1237644584 -3600
# Node ID dba663f1afa812fce43872bce69dd63fbc227fac
# Parent  3d62ef3a27e61f90201069495598e955b42a9a02
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).

diff -r 3d62ef3a27e6 -r dba663f1afa8 src/Pure/ML-Systems/ml_pretty.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_pretty.ML	Sat Mar 21 15:09:44 2009 +0100
@@ -0,0 +1,22 @@
+(*  Title:      Pure/ML-Systems/ml_pretty.ML
+    Author:     Makarius
+
+Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in
+Poly/ML 5.3).
+*)
+
+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;
+
+end;
+