From 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jul 2015 10:36:12 +0200 Subject: Imported Upstream version 8.5~beta2+dfsg --- printing/ppconstrsig.mli | 2 -- printing/pptactic.mli | 5 ++-- printing/pptacticsig.mli | 1 - printing/ppvernac.ml | 17 ++++++++++---- printing/prettyp.ml | 14 ++++++----- printing/printer.ml | 61 ++++++++++++++++++++++++++++++------------------ printing/printer.mli | 6 +++-- printing/richprinter.ml | 7 +++--- printing/richprinter.mli | 4 +--- 9 files changed, 69 insertions(+), 48 deletions(-) (limited to 'printing') diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli index 15413d51..b7eb9b1f 100644 --- a/printing/ppconstrsig.mli +++ b/printing/ppconstrsig.mli @@ -12,8 +12,6 @@ open Libnames open Constrexpr open Names open Misctypes -open Locus -open Genredexpr module type Pp = sig diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 284237f0..fa91aefc 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -15,9 +15,7 @@ open Names open Constrexpr open Tacexpr open Ppextend -open Environ -open Pattern -open Misctypes + type 'a raw_extra_genarg_printer = (constr_expr -> std_ppcmds) -> @@ -63,3 +61,4 @@ include Pptacticsig.Pp located in {!Ppannotation.t}. *) module Richpp : Pptacticsig.Pp +val ltop : tolerability diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 98b5757d..166a6675 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -8,7 +8,6 @@ open Pp open Genarg -open Names open Constrexpr open Tacexpr open Ppextend diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e9e335ec..89ffae4b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -740,9 +740,14 @@ module Make | VernacEndProof (Proved (opac,o)) -> return ( match o with - | None -> if opac then keyword "Qed" else keyword "Defined" + | None -> (match opac with + | Transparent -> keyword "Defined" + | Opaque None -> keyword "Qed" + | Opaque (Some l) -> + keyword "Qed" ++ spc() ++ str"export" ++ + prlist_with_sep (fun () -> str", ") pr_lident l) | Some (id,th) -> (match th with - | None -> (if opac then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id + | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id) ) | VernacExactProof c -> @@ -858,10 +863,14 @@ module Make | VernacNameSectionHypSet (id,set) -> return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++ str ":="++spc()++pr_using set)) - | VernacRequire (exp, l) -> + | VernacRequire (from, exp, l) -> + let from = match from with + | None -> mt () + | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc () + in return ( hov 2 - (keyword "Require" ++ spc() ++ pr_require_token exp ++ + (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++ prlist_with_sep sep pr_module l) ) | VernacImport (f,l) -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 223377c2..4a66c33d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -109,7 +109,7 @@ let print_impargs_list prefix l = [(if ismt prefix then str "When" else prefix ++ str ", when") ++ str " applied to " ++ (if Int.equal n1 n2 then int_or_no n2 else - if Int.equal n1 0 then str "less than " ++ int n2 + if Int.equal n1 0 then str "no more than " ++ int n2 else int n1 ++ str " to " ++ int_or_no n2) ++ str (String.plural n2 " argument") ++ str ":"; v 0 (prlist_with_sep cut (fun x -> x) @@ -197,11 +197,13 @@ let print_opacity ref = let print_polymorphism ref = let poly = Global.is_polymorphic ref in let template_poly = Global.is_template_polymorphic ref in - pr_global ref ++ str " is " ++ str + if Flags.is_universe_polymorphism () || poly || template_poly then + [ pr_global ref ++ str " is " ++ str (if poly then "universe polymorphic" else if template_poly then "template universe polymorphic" - else "not universe polymorphic") + else "not universe polymorphic") ] + else [] let print_primitive_record mipv = function | Some (Some (_, ps,_)) -> @@ -214,9 +216,8 @@ let print_primitive ref = let mib,_ = Global.lookup_inductive ind in print_primitive_record mib.mind_packets mib.mind_record | _ -> [] - + let print_name_infos ref = - let poly = print_polymorphism ref in let impls = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in let renames = @@ -228,7 +229,8 @@ let print_name_infos ref = print_ref true ref; blankline] else [] in - poly :: print_primitive ref @ + print_polymorphism ref @ + print_primitive ref @ type_info_for_implicit @ print_renames_list (mt()) renames @ print_impargs_list (mt()) impls @ diff --git a/printing/printer.ml b/printing/printer.ml index 3403fb9c..0d3a1c17 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -11,7 +11,6 @@ open Errors open Util open Names open Term -open Vars open Environ open Globnames open Nametab @@ -446,6 +445,16 @@ let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ i let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs) +(* Display a list of evars given by their name, with a prefix *) +let pr_ne_evar_set hd tl sigma l = + if l != Evar.Set.empty then + let l = Evar.Set.fold (fun ev -> + Evar.Map.add ev (Evarutil.nf_evar_info sigma (Evd.find sigma ev))) + l Evar.Map.empty in + hd ++ pr_evars sigma l ++ tl + else + mt () + let default_pr_subgoal n sigma = let rec prrec p = function | [] -> error "No such goal." @@ -535,26 +544,27 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals else pr_rec 1 (g::l) in + (* Side effect! This has to be made more robust *) + let () = + match close_cmd with + | Some cmd -> msg_info cmd + | None -> () + in match goals with | [] -> begin - match close_cmd with - Some cmd -> - (str "Subproof completed, now type " ++ str cmd ++ - str ".") - | None -> - let exl = Evarutil.non_instantiated sigma in - if Evar.Map.is_empty exl then - (str"No more subgoals." - ++ emacs_print_dependent_evars sigma seeds) - else - let pei = pr_evars_int sigma 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + let exl = Evarutil.non_instantiated sigma in + if Evar.Map.is_empty exl then + (str"No more subgoals." + ++ emacs_print_dependent_evars sigma seeds) + else + let pei = pr_evars_int sigma 1 exl in + (str "No more subgoals but non-instantiated existential " ++ + str "variables:" ++ fnl () ++ (hov 0 pei) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + str "You can use Grab Existential Variables.") end - | [g] when not !Flags.print_emacs -> + | [g] when not !Flags.print_emacs && pr_first -> let pg = default_pr_goal { it = g ; sigma = sigma; } in v 0 ( str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra @@ -563,8 +573,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals ) | g1::rest -> let goals = print_multiple_goals g1 rest in + let ngoals = List.length rest+1 in v 0 ( - int(List.length rest+1) ++ focused_if_needed ++ str"subgoals" ++ + int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ print_extra ++ str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1") ++ pr_goal_tag g1 @@ -578,7 +589,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals type printer_pr = { - pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; } @@ -622,10 +633,14 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf | _ , _, _ -> - msg_info (str "This subproof is complete, but there are still unfocused goals." ++ - (match Proof_global.Bullet.suggest p - with None -> str"" | Some s -> fnl () ++ str s)); - fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals + let end_cmd = + strbrk "This subproof is complete, but there are still \ + unfocused goals." ++ + (match Proof_global.Bullet.suggest p + with None -> str"" | Some s -> fnl () ++ str s) ++ + fnl () + in + pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals end | _ -> pr_subgoals None sigma seeds shelf stack goals end diff --git a/printing/printer.mli b/printing/printer.mli index 6b9c7081..a469a8db 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -128,7 +128,7 @@ val pr_transparent_state : transparent_state -> std_ppcmds (** Proofs *) val pr_goal : goal sigma -> std_ppcmds -val pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds +val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds val pr_concl : int -> evar_map -> goal -> std_ppcmds @@ -137,6 +137,8 @@ val pr_nth_open_subgoal : int -> std_ppcmds val pr_evar : evar_map -> (evar * evar_info) -> std_ppcmds val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds val pr_evars : evar_map -> evar_info Evar.Map.t -> std_ppcmds +val pr_ne_evar_set : std_ppcmds -> std_ppcmds -> evar_map -> + Evar.Set.t -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds @@ -166,7 +168,7 @@ val pr_assumptionset : val pr_goal_by_id : string -> std_ppcmds type printer_pr = { - pr_subgoals : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; };; diff --git a/printing/richprinter.ml b/printing/richprinter.ml index d71dc82d..d95e1907 100644 --- a/printing/richprinter.ml +++ b/printing/richprinter.ml @@ -5,21 +5,20 @@ module RichppVernac = Ppvernac.Richpp module RichppTactic = Pptactic.Richpp type rich_pp = - string - * Ppannotation.t Richpp.located Xml_datatype.gxml + 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 raw_pp, rich_pp = + 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 - (raw_pp, rich_pp, xml) + (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 index c67d52c0..41c31351 100644 --- a/printing/richprinter.mli +++ b/printing/richprinter.mli @@ -20,12 +20,10 @@ (** A rich pretty-print is composed of: *) type rich_pp = - (** - a raw pretty-print ; *) - string (** - a generalized semi-structured document whose attributes are annotations ; *) - * Ppannotation.t Richpp.located Xml_datatype.gxml + Ppannotation.t Richpp.located Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) -- cgit v1.2.3