diff options
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 48 |
1 files changed, 23 insertions, 25 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6e5b048c..a3d5cf5c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -29,7 +29,7 @@ let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) -let pppp x = pp x +let pp x = Pp.pp_with !Pp_control.std_ft x (** Future printer *) @@ -40,10 +40,10 @@ let ppid id = pp (pr_id id) let pplab l = pp (pr_lab l) let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) let ppdir dir = pp (pr_dirpath dir) -let ppmp mp = pp(str (string_of_mp mp)) +let ppmp mp = pp(str (ModPath.debug_to_string mp)) let ppcon con = pp(debug_pr_con con) let ppproj con = pp(debug_pr_con (Projection.constant con)) -let ppkn kn = pp(pr_kn kn) +let ppkn kn = pp(str (KerName.to_string kn)) let ppmind kn = pp(debug_pr_mind kn) let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i) let ppsp sp = pp(pr_path sp) @@ -79,7 +79,7 @@ let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr x)) let pppattern = (fun x -> pp(pr_constr_pattern x)) let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e))) -let ppfconstr c = ppconstr (Closure.term_of_fconstr c) +let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; @@ -215,13 +215,12 @@ let ppuniverse_subst l = pp (Univ.pr_universe_subst l) let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) -let ppconstraints_map c = pp (Universes.pr_constraints_map c) let ppconstraints c = pp (pr_constraints Level.pr c) let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx -let ppuniverses u = pp (Univ.pr_universes Level.pr u) +let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) @@ -315,7 +314,7 @@ let constr_display csr = | Anonymous -> "Anonymous" in - Pp.pp (str (term_display csr) ++fnl ()); Pp.pp_flush () + pp (str (term_display csr) ++fnl ()) open Format;; @@ -456,7 +455,7 @@ let print_pure_constr csr = print_string (Printexc.to_string e);print_flush (); raise e -let ppfconstr c = ppconstr (Closure.term_of_fconstr c) +let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" @@ -467,16 +466,19 @@ let pp_generic_argument arg = pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">") let prgenarginfo arg = - let tpe = pr_argument_type (genarg_tag arg) in - let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in - try - let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in - str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" - with _any -> + let Geninterp.Val.Dyn (tag, _) = arg in + let tpe = Geninterp.Val.pr tag in + (** FIXME *) +(* try *) +(* let data = Pptactic.pr_top_generic (Global.env ()) arg in *) +(* str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" *) +(* with _any -> *) str "<genarg:" ++ tpe ++ str ">" let ppgenarginfo arg = pp (prgenarginfo arg) +let ppgenargargt arg = pp (str (Genarg.ArgT.repr arg)) + let ppist ist = let pr id arg = prgenarginfo arg in pp (pridmap pr ist.Geninterp.lfun) @@ -485,9 +487,7 @@ let ppist ist = (* Vernac-level debugging commands *) let in_current_context f c = - let (evmap,sign) = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in + let (evmap,sign) = Pfedit.get_current_context () in f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*) (* We expand the result of preprocessing to be independent of camlp4 @@ -509,35 +509,33 @@ let _ = try Vernacinterp.vinterp_add false ("PrintConstr", 0) (function - [c] when genarg_tag c = ConstrArgType && true -> + [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Pp.pp (Errors.print e) + e -> pp (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintConstr", 0) None [GramTerminal "PrintConstr"; GramNonTerminal - (Loc.ghost,ConstrArgType,Aentry ("constr","constr"), - Some (Names.Id.of_string "c"))] + (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] let _ = try Vernacinterp.vinterp_add false ("PrintPureConstr", 0) (function - [c] when genarg_tag c = ConstrArgType && true -> + [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") with - e -> Pp.pp (Errors.print e) + e -> pp (CErrors.print e) let _ = extend_vernac_command_grammar ("PrintPureConstr", 0) None [GramTerminal "PrintPureConstr"; GramNonTerminal - (Loc.ghost,ConstrArgType,Aentry ("constr","constr"), - Some (Names.Id.of_string "c"))] + (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)] (* Setting printer of unbound global reference *) open Names |