X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationPp.ml;h=8f1db4a62e3ef2311fcba6f41b0b3d6751a75f18;hb=2914bfbeac3c2e0f53ba8c612cd11b3b2afbabce;hp=99255465d0fdcff99268d365ad64e274adac50b7;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git

diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml
index 99255465d..8f1db4a62 100644
--- a/matitaB/components/content/notationPp.ml
+++ b/matitaB/components/content/notationPp.ml
@@ -70,7 +70,8 @@ let pp_attribute =
           (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
   | `Level (prec) -> sprintf "L(%d)" prec 
   | `Raw _ -> "R"
-  | `Loc _ -> "@"
+  | `Loc l -> let x,y = HExtlib.loc_of_floc l in 
+              "@" ^ (string_of_int x) ^ "," ^ (string_of_int y)
   | `ChildPos p -> sprintf "P(%s)" (pp_pos p)
 
 let pp_capture_variable pp_term = 
@@ -79,6 +80,7 @@ let pp_capture_variable pp_term =
   | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")"
 
 let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
+ let debug_printing = true in
   let pp_ident = function
   | Ast.Ident (id,`Ambiguous) -> "A:" ^ id
   | Ast.Ident (id,`Rel) -> "R:" ^ id
@@ -90,7 +92,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     match t with
     | 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 (`Raw text, t) -> "RAW:(" ^ (pp_term t) ^ ")"
     | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
     | Ast.Appl terms ->
         sprintf "%s" (String.concat " " (List.map pp_term terms))
@@ -114,7 +116,7 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
           | None -> ""
           | Some (ty, href_opt) ->
               sprintf " in %s%s" ty
-              (match debug_printing, href_opt with
+              (match (*debug_printing*) true, href_opt with
               | true, Some uri ->
                   sprintf "(i.e.%s)" (NReference.string_of_reference uri)
               | _ -> ""))	  
@@ -164,14 +166,15 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | Ast.Sort `Prop -> "Prop"
     | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
     | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
-    | Ast.Symbol (name, _) -> "'" ^ name
+    | Ast.Symbol (name, None) -> "'" ^ name
+    | Ast.Symbol (name, Some (_,desc)) -> "'" ^ name ^ ":" ^ desc
 
     | Ast.UserInput -> "%"
 
-    | Ast.Literal l -> pp_literal l
-    | Ast.Layout l -> pp_layout status l
-    | Ast.Magic m -> pp_magic status m
-    | Ast.Variable v -> pp_variable v
+    | Ast.Literal l -> "literal:(" ^ (pp_literal l) ^ ")"
+    | Ast.Layout l -> "layout:(" ^ (pp_layout status l) ^ ")"
+    | Ast.Magic m -> "magic:(" ^ (pp_magic status m) ^ ")"
+    | Ast.Variable v -> "variable:" ^ (pp_variable v)
   in
   match pp_parens, t with
     | false, _ 
@@ -190,8 +193,9 @@ and pp_pattern status =
     Ast.Pattern (head, href, vars), term ->
      let head_pp =
        head ^
-       (match debug_printing, href with
+       (match (*debug_printing*)true, href with
        | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri)
+       | true, None -> "(i.e.ambiguous)"
        | _ -> "")
      in
      sprintf "%s \\Rightarrow %s"
@@ -343,6 +347,7 @@ let rec pp_value (status: #NCic.status) = function
   | Env.OptValue (Some v) -> "Some " ^ pp_value status v
   | Env.OptValue None -> "None"
   | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map (pp_value status) l))
+  | Env.DisambiguationValue _ -> sprintf "#"
 
 let rec pp_value_type =
   function
@@ -351,6 +356,7 @@ let rec pp_value_type =
   | Env.NumType -> "Number"
   | Env.OptType t -> "Maybe " ^ pp_value_type t
   | Env.ListType l -> "List " ^ pp_value_type l
+  | Env.NoType -> "NoType"
 
 let pp_env status env =
   String.concat "; "