cosmetic changes;
authorwenzelm
Wed, 19 Jan 1994 14:13:23 +0100
changeset 235 775dd81a58e5
parent 234 1b3bee8d5d7e
child 236 d33cd0011e48
cosmetic changes;
src/Pure/Syntax/README
src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/README	Wed Jan 19 14:12:40 1994 +0100
+++ b/src/Pure/Syntax/README	Wed Jan 19 14:13:23 1994 +0100
@@ -5,9 +5,10 @@
 following structures are supposed to be exported:
 
   Pretty        (generic pretty printing module)
+  Scanner       (generic scanner toolbox)
+
   Syntax        (interface to the syntax module)
   BasicSyntax   (part of Syntax made pervasive)
-  Scanner       (generic scanner toolbox)
 
 There is no Makefile to compile these files separately; they are compiled as
 part of Pure Isabelle.
--- a/src/Pure/Syntax/ast.ML	Wed Jan 19 14:12:40 1994 +0100
+++ b/src/Pure/Syntax/ast.ML	Wed Jan 19 14:13:23 1994 +0100
@@ -84,8 +84,7 @@
 fun pretty_ast (Constant a) = Pretty.str (quote a)
   | pretty_ast (Variable x) = Pretty.str x
   | pretty_ast (Appl asts) =
-      Pretty.blk (2, (Pretty.str "(") ::
-        (separate (Pretty.brk 1) (map pretty_ast asts)) @ [Pretty.str ")"]);
+      Pretty.parents "(" ")" (Pretty.breaks (map pretty_ast asts));
 
 
 (* pprint_ast *)
@@ -96,8 +95,7 @@
 (* pretty_rule *)
 
 fun pretty_rule (lhs, rhs) =
-  Pretty.blk
-    (2, [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs]);
+  Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
 
 
 (* head_of_ast, head_of_rule *)
@@ -212,8 +210,6 @@
     val failed_matches = ref 0;
     val changes = ref 0;
 
-    fun inc i = i := ! i + 1;
-
     fun subst _ (ast as Constant _) = ast
       | subst env (Variable x) = Env.get (env, x)
       | subst env (Appl asts) = Appl (map (subst env) asts);