From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 27 Sep 2005 14:31:40 +0000 (+0000)
Subject: more fine grained debug printing
X-Git-Tag: V_0_7_2_3~294
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=67682791e43d61b862e4b442e1e8ae5561df134b;p=helm.git

more fine grained debug printing
---

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 0bda68846..4183d003f 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -52,6 +52,12 @@ let pp_literal =
       | `Keyword s
       | `Number s -> s)
 
+let pp_assoc =
+  function
+  | Gramext.NonA -> "N"
+  | Gramext.LeftA -> "L"
+  | Gramext.RightA -> "R"
+
 let rec pp_term ?(pp_parens = true) t =
   let t_pp =
     match t with
@@ -62,8 +68,14 @@ let rec pp_term ?(pp_parens = true) t =
           (String.concat ";"
             (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
           (pp_term ~pp_parens:false term)
-    | Ast.AttributedTerm (_, term) when debug_printing ->
+    | Ast.AttributedTerm (`Level (prec, assoc), term) when debug_printing ->
+        sprintf "L(%d%s)[%s]" prec (pp_assoc assoc)
+          (pp_term ~pp_parens:false term)
+    | Ast.AttributedTerm (`Raw _, term) when debug_printing ->
+        sprintf "R[%s]" (pp_term ~pp_parens:false term)
+    | Ast.AttributedTerm (`Loc _, term) when debug_printing ->
         sprintf "@[%s]" (pp_term ~pp_parens:false term)
+
     | Ast.AttributedTerm (`Raw text, _) -> text
     | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term