diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 262 | ||||
| -rw-r--r-- | printing/pptactic.mli | 7 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 7 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | printing/printer.ml | 52 | ||||
| -rw-r--r-- | printing/printing.mllib | 4 | ||||
| -rw-r--r-- | printing/printmod.ml | 1 | ||||
| -rw-r--r-- | printing/richprinter.ml | 24 | ||||
| -rw-r--r-- | printing/richprinter.mli | 36 |
9 files changed, 151 insertions, 248 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 19536d9f83..5356cdee8a 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -14,6 +14,7 @@ open Util open Constrexpr open Tacexpr open Genarg +open Geninterp open Constrarg open Libnames open Ppextend @@ -26,23 +27,20 @@ open Printer let pr_global x = Nametab.pr_global_env Id.Set.empty x -type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list +type 'a grammar_tactic_prod_item_expr = +| TacTerm of string +| TacNonTerm of Loc.t * 'a * Names.Id.t + +type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { pptac_level : int; pptac_prods : grammar_terminals; } -(* ML Extensions *) -let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t = - Hashtbl.create 17 - (* Tactic notations *) let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty -let declare_ml_tactic_pprule key pt = - Hashtbl.add prtac_tab key pt - let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab @@ -104,23 +102,38 @@ module Make let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) - let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with - | Val.List tag -> - pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x - | Val.Opt tag -> pr_opt_no_spc (fun x -> pr_value lev (Val.Dyn (tag, x))) x - | Val.Pair (tag1, tag2) -> - str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++ - pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")" - | Val.Base t -> - let name = Val.repr t in - let default = str "<" ++ str name ++ str ">" in - match ArgT.name name with - | None -> default - | Some (ArgT.Any arg) -> - let wit = ExtraArg arg in - match Val.eq (val_tag (Topwit wit)) (Val.Base t) with + let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with + | None -> false + | Some _ -> true + + let unbox : type a. Val.t -> a Val.typ -> a= fun (Val.Dyn (tag, x)) t -> + match Val.eq tag t with + | None -> assert false + | Some Refl -> x + + let rec pr_value lev v : std_ppcmds = + if has_type v Val.typ_list then + pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list) + else if has_type v Val.typ_opt then + pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt) + else if has_type v Val.typ_pair then + let (v1, v2) = unbox v Val.typ_pair in + str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")" + else + let Val.Dyn (tag, x) = v in + let name = Val.repr tag in + let default = str "<" ++ str name ++ str ">" in + match ArgT.name name with | None -> default - | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) + | Some (ArgT.Any arg) -> + let wit = ExtraArg arg in + match val_tag (Topwit wit) with + | Val.Base t -> + begin match Val.eq t tag with + | None -> default + | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) + end + | _ -> default let pr_with_occurrences pr (occs,c) = match occs with @@ -326,59 +339,23 @@ module Make try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x) with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x) - let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) = - match wit with - | ListArg wit -> - let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in - let ans = pr_sequence map x in - hov_if_not_empty 0 ans - | OptArg wit -> - let ans = match x with - | None -> mt () - | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) - in - hov_if_not_empty 0 ans - | PairArg (wit1, wit2) -> - let p, q = x in - let p = in_gen (topwit wit1) p in - let q = in_gen (topwit wit2) q in - let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in - hov_if_not_empty 0 ans - | ExtraArg s -> - try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x) - with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x) - let rec tacarg_using_rule_token pr_gen = function - | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al) - | Egramml.GramNonTerminal _ :: l, a :: al -> - let r = tacarg_using_rule_token pr_gen (l,al) in - pr_gen a :: r - | [], [] -> [] - | _ -> failwith "Inconsistent arguments of extended tactic" - - let filter_arg = function - | Egramml.GramTerminal _ -> None - | Egramml.GramNonTerminal (_, Rawwit t, _) -> Some (ArgumentType t) + | [] -> [] + | TacTerm s :: l -> keyword s :: tacarg_using_rule_token pr_gen l + | TacNonTerm (_, (symb, arg), _) :: l -> + pr_gen symb arg :: tacarg_using_rule_token pr_gen l let pr_tacarg_using_rule pr_gen l = let l = match l with - | (Egramml.GramTerminal s :: l, al) -> + | TacTerm s :: l -> (** First terminal token should be considered as the name of the tactic, so we tag it differently than the other terminal tokens. *) - primitive s :: (tacarg_using_rule_token pr_gen (l, al)) + primitive s :: tacarg_using_rule_token pr_gen l | _ -> tacarg_using_rule_token pr_gen l in pr_sequence (fun x -> x) l - let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l = - try - let pp_rules = Hashtbl.find prtac_tab s in - let pp = pp_rules.(i) in - let args = List.map_filter filter_arg pp.pptac_prods in - let () = if not (List.for_all2eq check args l) then raise Not_found in - let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in - if pp.pptac_level > lev then surround p else p - with Not_found -> + let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ str "@" ++ int i @@ -389,31 +366,99 @@ module Make in str "<" ++ name ++ str ">" ++ args - let pr_alias_gen check pr_gen lev key l = + let pr_alias_key key = + try + let prods = (KNmap.find key !prnotation_tab).pptac_prods in + (* First printing strategy: only the head symbol *) + match prods with + | TacTerm s :: prods -> str s + | _ -> + (* Second printing strategy; if ever Tactic Notation is eventually *) + (* accepting notations not starting with an identifier *) + let rec pr = function + | [] -> [] + | TacTerm s :: prods -> s :: pr prods + | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in + str (String.concat " " (pr prods)) + with Not_found -> + KerName.print key + + let pr_alias_gen pr_gen lev key l = try let pp = KNmap.find key !prnotation_tab in - let args = List.map_filter filter_arg pp.pptac_prods in - let () = if not (List.for_all2eq check args l) then raise Not_found in - let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in + let rec pack prods args = match prods, args with + | [], [] -> [] + | TacTerm s :: prods, args -> TacTerm s :: pack prods args + | TacNonTerm (loc, symb, id) :: prods, arg :: args -> + TacNonTerm (loc, (symb, arg), id) :: pack prods args + | _ -> raise Not_found + in + let prods = pack pp.pptac_prods l in + let p = pr_tacarg_using_rule pr_gen prods in if pp.pptac_level > lev then surround p else p with Not_found -> - KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" - - let check_type t arg = match arg with - | TacGeneric arg -> argument_type_eq t (genarg_tag arg) - | _ -> argument_type_eq t (ArgumentType wit_tactic) + let pr arg = str "_" in + KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.ghost, arg)) + let is_genarg tag wit = + let ArgT.Any tag = tag in + argument_type_eq (ArgumentType (ExtraArg tag)) wit + + let get_list : type l. l generic_argument -> l generic_argument list option = + function (GenArg (wit, arg)) -> match wit with + | Rawwit (ListArg wit) -> Some (List.map (in_gen (rawwit wit)) arg) + | Glbwit (ListArg wit) -> Some (List.map (in_gen (glbwit wit)) arg) + | _ -> None + + let get_opt : type l. l generic_argument -> l generic_argument option option = + function (GenArg (wit, arg)) -> match wit with + | Rawwit (OptArg wit) -> Some (Option.map (in_gen (rawwit wit)) arg) + | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg) + | _ -> None + + let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds = + fun prtac symb arg -> match symb with + | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg + | Extend.Ulist1 s | Extend.Ulist0 s -> + begin match get_list arg with + | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | Some l -> pr_sequence (pr_any_arg prtac s) l + end + | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) -> + begin match get_list arg with + | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l + end + | Extend.Uopt s -> + begin match get_opt arg with + | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | Some l -> pr_opt (pr_any_arg prtac s) l + end + | Extend.Uentry _ | Extend.Uentryl _ -> + str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + + let rec pr_targ prtac symb arg = match symb with + | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> + prtac (1, Any) arg + | Extend.Uentryl (_, l) -> prtac (l, Any) arg + | _ -> + match arg with + | TacGeneric arg -> + let pr l arg = prtac l (TacGeneric arg) in + pr_any_arg pr symb arg + | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + let pr_raw_extend_rec prc prlc prtac prpat = - pr_extend_gen check_type (pr_farg prtac) + pr_extend_gen (pr_farg prtac) let pr_glob_extend_rec prc prlc prtac prpat = - pr_extend_gen check_type (pr_farg prtac) + pr_extend_gen (pr_farg prtac) - let pr_raw_alias prc prlc prtac prpat = - pr_alias_gen check_type (pr_farg prtac) - let pr_glob_alias prc prlc prtac prpat = - pr_alias_gen check_type (pr_farg prtac) + let pr_raw_alias prc prlc prtac prpat lev key args = + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args + let pr_glob_alias prc prlc prtac prpat lev key args = + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.ghost, a)))) lev key args (**********************************************************************) (* The tactic printer *) @@ -788,7 +833,6 @@ module Make (* Printing tactics as arguments *) let rec pr_atom0 a = tag_atom a (match a with | TacIntroPattern [] -> primitive "intros" - | TacIntroMove (None,MoveLast) -> primitive "intro" | t -> str "(" ++ pr_atom1 t ++ str ")" ) @@ -800,15 +844,6 @@ module Make | TacIntroPattern (_::_ as p) -> hov 1 (primitive "intros" ++ spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) - | TacIntroMove (None,MoveLast) as t -> - pr_atom0 t - | TacIntroMove (Some id,MoveLast) -> - primitive "intro" ++ spc () ++ pr_id id - | TacIntroMove (ido,hto) -> - hov 1 (primitive "intro" ++ pr_opt pr_id ido ++ - Miscprint.pr_move_location pr.pr_name hto) - | TacExact c -> - hov 1 (primitive "exact" ++ pr_constrarg c) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ @@ -881,23 +916,6 @@ module Make pr_opt (pr_clauses None pr.pr_name) cl) l ++ pr_opt pr_eliminator el ) - | TacDoubleInduction (h1,h2) -> - hov 1 ( - primitive "double induction" - ++ pr_arg pr_quantified_hypothesis h1 - ++ pr_arg pr_quantified_hypothesis h2 - ) - - (* Context management *) - | TacRename l -> - hov 1 ( - primitive "rename" ++ brk (1,1) - ++ prlist_with_sep - (fun () -> str "," ++ brk (1,1)) - (fun (i1,i2) -> - pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2) - l - ) (* Conversion *) | TacReduce (r,h) -> @@ -1203,7 +1221,7 @@ module Make let pr_and_constr_expr pr (c,_) = pr c - let pr_pat_and_constr_expr pr ((c,_),_) = pr c + let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c let pr_glob_tactic_level env n t = let glob_printers = @@ -1277,10 +1295,6 @@ module Make (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) - let pr_top_generic env = pr_top_generic_rec - (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - pr_value pr_constr_pattern - let pr_raw_extend env = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr @@ -1288,20 +1302,11 @@ module Make (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) - let check_val_type t arg = - let ArgumentType t = t in -(* let t = Genarg.val_tag (Obj.magic t) in *) -(* let Val.Dyn (t', _) = arg in *) -(* match Genarg.Val.eq t t' with *) -(* | None -> false *) -(* | Some _ -> true *) - true (** FIXME *) - let pr_alias pr lev key args = - pr_alias_gen check_val_type pr lev key args + pr_alias_gen (fun _ arg -> pr arg) lev key args let pr_extend pr lev ml args = - pr_extend_gen check_val_type pr lev ml args + pr_extend_gen pr lev ml args let pr_atomic_tactic env = pr_atomic_tactic_level env ltop @@ -1364,8 +1369,6 @@ let () = (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) ; - Genprint.register_print0 Constrarg.wit_sort - pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 Constrarg.wit_constr Ppconstr.pr_constr_expr @@ -1393,11 +1396,6 @@ let () = (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it))); - Genprint.register_print0 Constrarg.wit_constr_may_eval - (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr) - (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr) - (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr)) - pr_constr; Genprint.register_print0 Constrarg.wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 31a5a5d4a8..86e3ea5484 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -11,11 +11,15 @@ open Pp open Genarg +open Geninterp open Names open Constrexpr open Tacexpr open Ppextend +type 'a grammar_tactic_prod_item_expr = +| TacTerm of string +| TacNonTerm of Loc.t * 'a * Names.Id.t type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> @@ -41,14 +45,13 @@ val declare_extra_genarg_pprule : 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit -type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list +type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list type pp_tactic = { pptac_level : int; pptac_prods : grammar_terminals; } -val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit (** The default pretty-printers produce {!Pp.std_ppcmds} that are diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index d4858bac4f..c08d6044db 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -8,6 +8,7 @@ open Pp open Genarg +open Geninterp open Tacexpr open Ppextend open Environ @@ -35,8 +36,6 @@ module type Pp = sig val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds - val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds - val pr_raw_extend: env -> int -> ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds @@ -46,9 +45,13 @@ module type Pp = sig val pr_extend : (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + val pr_alias_key : Names.KerName.t -> std_ppcmds + val pr_alias : (Val.t -> std_ppcmds) -> int -> Names.KerName.t -> Val.t list -> std_ppcmds + val pr_alias_key : Names.KerName.t -> std_ppcmds + val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds val pr_raw_tactic : raw_tactic_expr -> std_ppcmds diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f0548238a7..cd7434843f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -99,11 +99,6 @@ module Make | ETBinder false -> str "closed binder" | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type" - let strip_meta id = - let s = Id.to_string id in - if s.[0] == '$' then Id.of_string (String.sub s 1 (String.length s - 1)) - else id - let pr_comment pr_c = function | CommentConstr c -> pr_c c | CommentString s -> qs s @@ -362,6 +357,7 @@ module Make | SetAssoc RightA -> keyword "right associativity" | SetAssoc NonA -> keyword "no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ + | SetOnlyPrinting -> keyword "only printing" | SetOnlyParsing Flags.Current -> keyword "only parsing" | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat("text",s) -> keyword "format " ++ pr_located qs s diff --git a/printing/printer.ml b/printing/printer.ml index 22bc122bd5..cc8da4097d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -28,10 +28,7 @@ let delayed_emacs_cmd s = if !Flags.print_emacs then s () else str "" let get_current_context () = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> - let env = Global.env () in - (Evd.from_env env, env) + Pfedit.get_current_context () (**********************************************************************) (** Terms *) @@ -384,16 +381,12 @@ let pr_transparent_state (ids, csts) = let default_pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in let env = Goal.V82.env sigma g in - let preamb,thesis,penv,pc = - mt (), mt (), - pr_context_of env sigma, - pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) - in - preamb ++ - str" " ++ hv 0 (penv ++ fnl () ++ - str (emacs_str "") ++ - str "============================" ++ fnl () ++ - thesis ++ str " " ++ pc) + let concl = Goal.V82.concl sigma g in + let goal = + pr_context_of env sigma ++ cut () ++ + str "============================" ++ cut () ++ + pr_goal_concl_style_env env sigma concl in + str " " ++ v 0 goal (* display a goal tag *) let pr_goal_tag g = @@ -555,7 +548,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals (* Side effect! This has to be made more robust *) let () = match close_cmd with - | Some cmd -> msg_info cmd + | Some cmd -> Feedback.msg_info cmd | None -> () in match goals with @@ -633,12 +626,12 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = begin match bgoals,shelf,given_up with | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals | [] , [] , _ -> - msg_info (str "No more subgoals, but there are some goals you gave up:"); + Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> - msg_info (str "All the remaining goals are on the shelf."); + Feedback.msg_info (str "All the remaining goals are on the shelf."); fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> @@ -689,35 +682,10 @@ let pr_prim_rule = function (str"cut " ++ pr_constr t ++ str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | FixRule (f,n,[],_) -> - (str"fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others,j) -> - if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth - | [] -> mt () in - (str"fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - - | Cofix (f,[],_) -> - (str"cofix " ++ pr_id f) - - | Cofix (f,others,j) -> - if not (Int.equal j 0) then msg_warning (strbrk "Unsupported printing of \"fix\""); - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) - | [] -> mt () in - (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) | Refine c -> str(if Termops.occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c - | Thin ids -> - (str"clear " ++ pr_sequence pr_id ids) - | Move (id1,id2) -> (str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2) diff --git a/printing/printing.mllib b/printing/printing.mllib index 652a34fa1f..bc8f0750e1 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -2,12 +2,8 @@ Genprint Pputils Ppannotation Ppconstr -Ppconstrsig Printer Pptactic -Pptacticsig Printmod Prettyp Ppvernac -Ppvernacsig -Richprinter diff --git a/printing/printmod.ml b/printing/printmod.ml index 9354cd28d0..5f98eeeab9 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -65,7 +65,6 @@ let get_new_id locals id = (** Inductive declarations *) -open Termops open Reduction let print_params env sigma params = diff --git a/printing/richprinter.ml b/printing/richprinter.ml deleted file mode 100644 index 5f39f36eab..0000000000 --- a/printing/richprinter.ml +++ /dev/null @@ -1,24 +0,0 @@ -open Richpp - -module RichppConstr = Ppconstr.Richpp -module RichppVernac = Ppvernac.Richpp -module RichppTactic = Pptactic.Richpp - -type rich_pp = - Ppannotation.t Richpp.located Xml_datatype.gxml - * Xml_datatype.xml - -let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag - -let make_richpp pr ast = - let rich_pp = - rich_pp get_annotations (pr ast) - in - let xml = Ppannotation.( - xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp - ) - in - (rich_pp, xml) - -let richpp_vernac = make_richpp RichppVernac.pr_vernac -let richpp_constr = make_richpp RichppConstr.pr_constr_expr diff --git a/printing/richprinter.mli b/printing/richprinter.mli deleted file mode 100644 index c9e84e3eb4..0000000000 --- a/printing/richprinter.mli +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This module provides an entry point to "rich" pretty-printers that - produce pretty-printing as done by {!Printer} but with additional - annotations represented as a semi-structured document. - - To understand what are these annotations and how they are represented - as standard XML attributes, please refer to {!Ppannotation}. - - In addition to these annotations, each node of the semi-structured - document contains a [startpos] and an [endpos] attribute that - relate this node to the raw pretty-printing. - Please refer to {!Richpp} for more details. *) - -(** A rich pretty-print is composed of: *) -type rich_pp = - - (** - a generalized semi-structured document whose attributes are - annotations ; *) - Ppannotation.t Richpp.located Xml_datatype.gxml - - (** - an XML document, representing annotations as usual textual - XML attributes. *) - * Xml_datatype.xml - -(** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *) -val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp - -(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *) -val richpp_constr : Constrexpr.constr_expr -> rich_pp |