From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 30 May 2011 11:02:26 +0000 (+0000)
Subject: Debugging code to understand cases where the output notation is not
X-Git-Tag: make_still_working~2481
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=10c62d5b6703eddbc83b011b73f9540e47a2001f;p=helm.git

Debugging code to understand cases where the output notation is not
applied, is applied badly or it raises an assert failure.

Usually the problem is given by optional parts of the term. For instance,
in output all typing information is present and it _must_ be matched.
---

diff --git a/matita/components/content_pres/content2presMatcher.ml b/matita/components/content_pres/content2presMatcher.ml
index 8b613a524..ee62e06e6 100644
--- a/matita/components/content_pres/content2presMatcher.ml
+++ b/matita/components/content_pres/content2presMatcher.ml
@@ -105,7 +105,7 @@ struct
               name, (Env.NumType, Env.NumValue s)
           | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
               name, (Env.StringType, Env.StringValue (Env.Ident s))
-          | _ -> assert false)
+          | _ -> assert false (* activate the DEBUGGING CODE below *))
         pl tl
     with Invalid_argument _ -> assert false
 
@@ -157,7 +157,16 @@ struct
       in
       magichooser candidates
     in
+(* DEBUGGING CODE 
+fun input ->
+let (fst,_)::_ = rows in
+prerr_endline ("RIGA: " ^ NotationPp.pp_term (new NCicPp.status) fst);
+prerr_endline ("CONTRO: " ^ NotationPp.pp_term (new NCicPp.status) input);
+*)
     M.compiler rows' match_cb (fun _ -> None)
+(* DEBUGGING CODE 
+input
+*)
 
   and compile_magic = function
     | Ast.Fold (kind, p_base, names, p_rec) ->