| author | wenzelm |
| Thu, 04 Jun 2009 19:15:54 +0200 | |
| changeset 31433 | 12f5f6af3d2d |
| parent 30623 | 9ed1122d6cd2 |
| child 38635 | f76ad0771f67 |
| permissions | -rw-r--r-- |
|
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/ml_pretty.ML |
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
3 |
|
|
30623
9ed1122d6cd2
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents:
30622
diff
changeset
|
4 |
Raw datatype for ML pretty printing. |
|
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
5 |
*) |
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
6 |
|
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
7 |
structure ML_Pretty = |
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
8 |
struct |
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
9 |
|
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
10 |
datatype pretty = |
|
30623
9ed1122d6cd2
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents:
30622
diff
changeset
|
11 |
Block of (string * string) * pretty list * int | |
|
9ed1122d6cd2
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents:
30622
diff
changeset
|
12 |
String of string * int | |
|
9ed1122d6cd2
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents:
30622
diff
changeset
|
13 |
Break of bool * int; |
|
30622
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
14 |
|
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
15 |
end; |
|
dba663f1afa8
Datatype for ML pretty printing (cf. mlsource/MLCompiler/Pretty.sml in Poly/ML 5.3).
wenzelm
parents:
diff
changeset
|
16 |