# HG changeset patch
# User wenzelm
# Date 1237661924 -3600
# Node ID 9ed1122d6cd2bd52649a6a878ce8fd1bee2ae6dc
# Parent  dba663f1afa812fce43872bce69dd63fbc227fac
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;

diff -r dba663f1afa8 -r 9ed1122d6cd2 src/Pure/ML-Systems/ml_pretty.ML
--- 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;