From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 27 Sep 2005 16:34:36 +0000 (+0000)
Subject: added/exported pp_pos & pp_attribute
X-Git-Tag: V_0_7_2_3~290
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e4d0e879c6288190ae793e1425b1ed74e40346c4;p=helm.git

added/exported pp_pos & pp_attribute
---

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 4183d003f..e5ff1587f 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -54,31 +54,36 @@ let pp_literal =
 
 let pp_assoc =
   function
-  | Gramext.NonA -> "N"
-  | Gramext.LeftA -> "L"
-  | Gramext.RightA -> "R"
+  | 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 (`IdRef id, term) when debug_printing ->
-        sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term)
-    | Ast.AttributedTerm (`XmlAttrs attrs, term) when debug_printing ->
-        sprintf "X(%s)[%s]"
-          (String.concat ";"
-            (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
-          (pp_term ~pp_parens:false term)
-    | 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 (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)
diff --git a/helm/ocaml/cic_notation/cicNotationPp.mli b/helm/ocaml/cic_notation/cicNotationPp.mli
index ca22765f8..2fb05c51b 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.mli
+++ b/helm/ocaml/cic_notation/cicNotationPp.mli
@@ -29,3 +29,6 @@ val pp_env: CicNotationEnv.t -> string
 val pp_value: CicNotationEnv.value -> string
 val pp_value_type: CicNotationEnv.value_type -> string
 
+val pp_pos: CicNotationPt.child_pos -> string
+val pp_attribute: CicNotationPt.term_attribute -> string
+