X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2Fcontent2presMatcher.ml;h=ee62e06e696da3bac0573f286da335d3a6cc188a;hb=6248fe356b55750c565ef7f36a40e593338a3c43;hp=2a432d33255eb35d94e7f59a91361ac2cda62c11;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git diff --git a/matita/components/content_pres/content2presMatcher.ml b/matita/components/content_pres/content2presMatcher.ml index 2a432d332..ee62e06e6 100644 --- a/matita/components/content_pres/content2presMatcher.ml +++ b/matita/components/content_pres/content2presMatcher.ml @@ -67,8 +67,11 @@ struct | _ -> PatternMatcher.Constructor let tag_of_pattern = get_tag let tag_of_term t = get_tag t - let string_of_term = NotationPp.pp_term - let string_of_pattern = NotationPp.pp_term + + (* Debugging only *) + (*CSC: new NCicPp.status is the best I can do now *) + let string_of_term = NotationPp.pp_term (new NCicPp.status) + let string_of_pattern = NotationPp.pp_term (new NCicPp.status) end module M = PatternMatcher.Matcher (Pattern21) @@ -101,8 +104,8 @@ struct | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) -> name, (Env.NumType, Env.NumValue s) | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) -> - name, (Env.StringType, Env.StringValue s) - | _ -> assert false) + name, (Env.StringType, Env.StringValue (Env.Ident s)) + | _ -> assert false (* activate the DEBUGGING CODE below *)) pl tl with Invalid_argument _ -> assert false @@ -154,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) ->