implemented transformations on top of notation code

[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 639ae48e0e62e00d4f7be4c7f724fd1e577896e8..b126a3def6c38166107d2f1695a9afccb2262253 100644 (file)
--- 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 = true
 
 let pp_binder = function
   | `Lambda -> "lambda"
@@ -36,23 +40,23 @@ 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 (_, 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 +103,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 -> ""