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 8b613a524775a32bab105d8c59bc126e1d5c676a..ee62e06e696da3bac0573f286da335d3a6cc188a 100644 (file)
--- 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) ->