X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=b5a2e04f22a9b9e837ce4694a4d1a6234c815949;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=1c3ad438687b731a39a02833bcce8590c1ff6405;hpb=5c9e1997848c2f74297a5a243679f4bcb6ae0dc7;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 1c3ad4386..b5a2e04f2 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -32,7 +32,7 @@ module Env = CicNotationEnv
    * be added to the output of pp_term.
    * set to false if you need, for example, cut and paste from matitac output to
    * matitatop *)
-let debug_printing = false
+let debug_printing = true
 
 let pp_binder = function
   | `Lambda -> "lambda"
@@ -52,20 +52,38 @@ let pp_literal =
       | `Keyword s
       | `Number s -> s)
 
+let pp_assoc =
+  function
+  | Gramext.NonA -> "NonA"
+  | Gramext.LeftA -> "LeftA"
+  | Gramext.RightA -> "RightA"
+
+let pp_pos =
+  function
+(*      `None -> "`None" *)
+    | `Left -> "`Left"
+    | `Right -> "`Right"
+    | `Inner -> "`Inner"
+
+let pp_attribute =
+  function
+  | `IdRef id -> sprintf "x(%s)" id
+  | `XmlAttrs attrs ->
+      sprintf "X(%s)"
+        (String.concat ";"
+          (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
+  | `Level (prec, assoc) -> sprintf "L(%d%s)" prec (pp_assoc assoc)
+  | `Raw _ -> "R"
+  | `Loc _ -> "@"
+  | `ChildPos p -> sprintf "P(%s)" (pp_pos p)
+
 let rec pp_term ?(pp_parens = true) t =
   let t_pp =
     match t with
-    | Ast.AttributedTerm (`Href hrefs, term) when debug_printing ->
-        sprintf "#(%s)[%s]"
-          (String.concat "," (List.map UriManager.string_of_uri hrefs))
-          (pp_term ~pp_parens:false term)
-    | Ast.AttributedTerm (`IdRef id, term) when debug_printing ->
-        sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term)
-    | Ast.AttributedTerm (_, term) when debug_printing ->
-        sprintf "@[%s]" (pp_term ~pp_parens:false term)
+    | Ast.AttributedTerm (attr, term) when debug_printing ->
+        sprintf "%s[%s]" (pp_attribute attr) (pp_term ~pp_parens:false term)
     | Ast.AttributedTerm (`Raw text, _) -> text
     | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
-
     | Ast.Appl terms ->
         sprintf "%s" (String.concat " " (List.map pp_term terms))
     | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body)