# 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;