X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPp.ml;h=9118d1c11d359c4c9767252ee0cb7e290cd6ab9e;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=639ae48e0e62e00d4f7be4c7f724fd1e577896e8;hpb=2817260358878e72fa359c6d2431b4c7c358a841;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 639ae48e0..9118d1c11 100644
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -28,7 +28,11 @@ open Printf
 open CicNotationEnv
 open CicNotationPt
 
-let print_attributes = true
+  (* when set to true debugging information, not in sync with input syntax, will
+   * 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 pp_binder = function
   | `Lambda -> "lambda"
@@ -36,23 +40,25 @@ let pp_binder = function
   | `Exists -> "exists"
   | `Forall -> "forall"
 
-(* let pp_literal = function  (* debugging version *)
+let pp_literal = function  (* debugging version *)
   | `Symbol s -> sprintf "symbol(%s)" s
   | `Keyword s -> sprintf "keyword(%s)" s
-  | `Number s -> sprintf "number(%s)" s *)
+  | `Number s -> sprintf "number(%s)" s
 
-let pp_literal = function
+(* let pp_literal = function
   | `Symbol s
   | `Keyword s
-  | `Number s -> s
+  | `Number s -> s *)
 
 let rec pp_term ?(pp_parens = true) t =
   let t_pp =
     match t with
-(*     | AttributedTerm (`Href _, term) when print_attributes ->
-        sprintf "#[%s]" (pp_term term)
-    | AttributedTerm (_, term) when print_attributes ->
-        sprintf "@[%s]" (pp_term term) *)
+    | AttributedTerm (`Href _, term) when debug_printing ->
+        sprintf "#[%s]" (pp_term ~pp_parens:false term)
+    | AttributedTerm (`IdRef id, term) when debug_printing ->
+        sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term)
+    | AttributedTerm (_, term) when debug_printing ->
+        sprintf "@[%s]" (pp_term ~pp_parens:false term)
     | AttributedTerm (`Raw text, _) -> text
     | AttributedTerm (_, term) -> pp_term ~pp_parens:false term
 
@@ -99,7 +105,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Sort `Prop -> "Prop"
     | Sort `Type -> "Type"
     | Sort `CProp -> "CProp"
-    | Symbol (name, _) -> name
+    | Symbol (name, _) -> "'" ^ name
 
     | UserInput -> ""