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

diff --git a/matitaB/components/content/notationPp.ml b/matitaB/components/content/notationPp.ml
index 99255465d..50ccb16b4 100644
--- a/matitaB/components/content/notationPp.ml
+++ b/matitaB/components/content/notationPp.ml
@@ -45,14 +45,12 @@ let pp_binder = function
 let pp_literal =
   if debug_printing then
     (function (* debugging version *)
-      | `Symbol s -> sprintf "symbol(%s)" s
-      | `Keyword s -> sprintf "keyword(%s)" s
-      | `Number s -> sprintf "number(%s)" s)
-  else
-    (function
-      | `Symbol s
-      | `Keyword s
-      | `Number s -> s)
+      | `Symbol _ as t -> 
+          sprintf "symbol(%s)" (NotationUtil.string_of_literal t)
+      | `Keyword _ as t -> 
+          sprintf "keyword(%s)" (NotationUtil.string_of_literal t)
+      | `Number _ as t -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
+  else NotationUtil.string_of_literal
 
 let pp_pos =
   function
@@ -70,7 +68,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 +78,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 +90,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 +114,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 +164,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, _ 
@@ -181,17 +182,14 @@ let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
     | true, Ast.Ident _    -> t_pp
     | _                    -> sprintf "(%s)" t_pp
 
-and pp_subst status (name, term) =
- sprintf "%s \\Assign %s" name (pp_term status term)
-and pp_substs status substs = String.concat "; " (List.map (pp_subst status) substs)
-
 and pp_pattern status =
  function
     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 +341,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 +350,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 "; "