Global PrintFilter -> MinimalLogger

1 files changed, 12 insertions, 6 deletions

diff --git a/misc/PPrinter.java b/misc/PPrinter.java
index eff2357..ad2842a 100644
--- a/misc/PPrinter.java
+++ b/misc/PPrinter.java
@@ -13,12 +13,16 @@ public class PPrinter<R,A> extends GJDepthFirst<R,A> {
     private int offset;
 
     private void printNode(Node n, A argu) {
+        String str = "";
         for (int i=0; i < this.offset; ++i)
-            PrintFilter.print(".", false);
-        PrintFilter.print(n.getClass().getSimpleName(), true);
+            str += ".";
+        MinimalLogger.info(String.format("%s%s",
+                                         str,
+                                         n.getClass().getSimpleName()));
         ++this.offset;
     }
 
+
     //
     // User-generated visitor methods below
     //
@@ -725,11 +729,13 @@ public class PPrinter<R,A> extends GJDepthFirst<R,A> {
     }
 
     public R visit(NodeToken n, A argu) {
+        String str = "";
         for (int i=0; i < this.offset; ++i)
-            PrintFilter.print(".", false);
-        PrintFilter.print(n.getClass().getSimpleName() +
-			  " => " +
-			  n.toString(), true);
+            str += ".";
+        MinimalLogger.info(String.format("%s%s => %s",
+                                         str,
+                                         n.getClass().getSimpleName(),
+                                         n.toString()));
         R _ret=null;
         return _ret;
     }