packaging cleanup: get rid of ancient debhelpers, use dh_install

[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 3118753f6088236ec11d182111555a235a96854d..9118d1c11d359c4c9767252ee0cb7e290cd6ab9e 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 = false
 
 let pp_binder = function
   | `Lambda -> "lambda"
@@ -36,26 +40,26 @@ 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 (`Raw (text, None), _) -> text
-    | AttributedTerm (`Raw (text, Some `Ast), _) -> sprintf "@{%s}" text
-    | AttributedTerm (`Raw (text, Some `Meta), _) -> sprintf "${%s}" text
+    | 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
 
     | Appl terms ->
@@ -101,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 -> ""