]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationPp.ml
Better handling of idref propagation, no more Href hack, multiple idrefs are
[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml
index 1c3ad438687b731a39a02833bcce8590c1ff6405..0bda688469725924a983aa1ecce547ffa9181c94 100644 (file)
@@ -55,12 +55,13 @@ let pp_literal =
 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 (`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 (_, term) when debug_printing ->
         sprintf "@[%s]" (pp_term ~pp_parens:false term)
     | Ast.AttributedTerm (`Raw text, _) -> text