diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 76 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 3 | ||||
| -rw-r--r-- | printing/printer.ml | 10 | ||||
| -rw-r--r-- | printing/printer.mli | 3 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 28 | ||||
| -rw-r--r-- | printing/proof_diffs.mli | 6 |
6 files changed, 90 insertions, 36 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index af105f4d63..e312c68b7d 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -77,8 +77,8 @@ let tag_var = tag Tag.variable | LevelSome -> true let prec_of_prim_token = function - | Numeral (NumTok.SPlus,_) -> lposint - | Numeral (NumTok.SMinus,_) -> lnegint + | Number (NumTok.SPlus,_) -> lposint + | Number (NumTok.SMinus,_) -> lnegint | String _ -> latom let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps = @@ -222,18 +222,54 @@ let tag_var = tag Tag.variable | t -> str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t let pr_prim_token = function - | Numeral n -> NumTok.Signed.print n + | Number n -> NumTok.Signed.print n | String s -> qs s let pr_evar pr id l = hov 0 ( - tag_evar (str "?" ++ pr_id id) ++ + tag_evar (str "?" ++ pr_lident id) ++ (match l with | [] -> mt() | l -> - let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in + let f (id,c) = pr_lident id ++ str ":=" ++ pr ltop c in str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) + (* Assuming "{" and "}" brackets, prints + - if there is enough room + { a; b; c } + - otherwise + { + a; + b; + c + } + Alternatively, replace outer hv with h to get instead: + { a; + b; + c } + Replace the inner hv with hov to respectively get instead (if enough room): + { + a; b; + c + } + or + { a; b; + c } + *) + let pr_record left right pr = function + | [] -> str left ++ str " " ++ str right + | l -> + hv 0 ( + str left ++ + brk (1,String.length left) ++ + hv 0 (prlist_with_sep pr_semicolon pr l) ++ + brk (1,0) ++ + str right) + + let pr_record_body left right pr l = + let pr_defined_field (id, c) = hov 2 (pr_reference id ++ str" :=" ++ pr c) in + pr_record left right pr_defined_field l + let las = lapp let lpator = 0 let lpatrec = 0 @@ -242,11 +278,7 @@ let tag_var = tag Tag.variable let rec pr_patt sep inh p = let (strm,prec) = match CAst.(p.v) with | CPatRecord l -> - let pp (c, p) = - pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p - in - (if l = [] then str "{| |}" - else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec + pr_record_body "{|" "|}" (pr_patt spc lpattop) l, lpatrec | CPatAlias (p, na) -> pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las @@ -287,6 +319,7 @@ let tag_var = tag Tag.variable | CPatDelimiters (k,p) -> pr_delimiters k (pr_patt mt lsimplepatt p), 1 + | CPatCast _ -> assert false in @@ -464,11 +497,6 @@ let tag_var = tag Tag.variable pr (LevelLt lapp) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) - let pr_record_body_gen pr l = - spc () ++ - prlist_with_sep pr_semicolon - (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l - let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc () let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc () @@ -568,10 +596,7 @@ let tag_var = tag Tag.variable | CApp ((None,a),l) -> return (pr_app (pr mt) a l, lapp) | CRecord l -> - return ( - hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), - latom - ) + return (pr_record_body "{|" "|}" (pr spc ltop) l, latom) | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( @@ -656,13 +681,10 @@ let tag_var = tag Tag.variable | CDelimiters (sc,a) -> return (pr_delimiters sc (pr mt (LevelLe ldelim) a), ldelim) | CArray(u, t,def,ty) -> - let pp = ref (str " |"++ spc () ++ pr mt ltop def - ++ pr_opt_type_spc (pr mt) ty ++ str " |]" ++ pr_universe_instance u) in - for i = Array.length t - 1 downto 1 do - pp := str ";" ++ pr mt ltop t.(i) ++ !pp - done; - pp := pr mt ltop t.(0) ++ !pp; - hov 0 (str "[|" ++ !pp), 0 + hov 0 (str "[| " ++ prvect_with_sep (fun () -> str "; ") (pr mt ltop) t ++ + (if not (Array.is_empty t) then str " " else mt()) ++ + str "|" ++ spc() ++ pr mt ltop def ++ pr_opt_type_spc (pr mt) ty ++ + str " |]" ++ pr_universe_instance u), 0 in let loc = constr_loc a in pr_with_comments ?loc @@ -717,7 +739,5 @@ let tag_var = tag Tag.variable let pr_cases_pattern_expr = pr_patt ltop - let pr_record_body = pr_record_body_gen pr - let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop) diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 2850e4bfa0..02e04573f8 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -41,7 +41,8 @@ val pr_guard_annot -> recursion_order_expr option -> Pp.t -val pr_record_body : (qualid * constr_expr) list -> Pp.t +val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t +val pr_record_body : string -> string -> ('a -> Pp.t) -> (Libnames.qualid * 'a) list -> Pp.t val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t val pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index a1a2d9ae51..ea718526de 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -45,6 +45,8 @@ let should_gname = ~key:["Printing";"Goal";"Names"] ~value:false +let print_goal_names = should_gname (* for export *) + (**********************************************************************) (** Terms *) @@ -765,9 +767,9 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map v 0 ( int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ print_extra - ++ str (if (should_gname()) then ", subgoal 1" else "") - ++ (if should_tag() then pr_goal_tag g1 else str"") - ++ pr_goal_name sigma g1 ++ cut () ++ goals + ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", subgoal 1" else "") + ++ (if pr_first && should_tag() then pr_goal_tag g1 else str"") + ++ (if pr_first then pr_goal_name sigma g1 else mt()) ++ cut () ++ goals ++ (if unfocused=[] then str "" else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut() ++ pr_rec (List.length rest + 2) unfocused)) @@ -884,7 +886,7 @@ struct MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 | TypeInType k1, TypeInType k2 -> - GlobRef.Ordered.compare k1 k2 + GlobRef.CanOrd.compare k1 k2 | Constant _, _ -> -1 | _, Constant _ -> 1 | Positive _, _ -> -1 diff --git a/printing/printer.mli b/printing/printer.mli index a25cbebe91..ea388ae57e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -264,3 +264,6 @@ val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t val pr_typing_flags : Declarations.typing_flags -> Pp.t + +(** Tells if flag "Printing Goal Names" is activated *) +val print_goal_names : unit -> bool diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 43f70dfecc..b2ebc61b4e 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -252,6 +252,9 @@ let pp_of_type env sigma ty = let pr_leconstr_env ?lax ?inctx ?scope env sigma t = Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) +let pr_econstr_env ?lax ?inctx ?scope env sigma t = + Ppconstr.pr_constr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t) + let pr_lconstr_env ?lax ?inctx ?scope env sigma c = pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c) @@ -511,12 +514,12 @@ let match_goals ot nt = | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> () | CPatVar _, CPatVar _ -> () | CEvar (n,l), CEvar (n2,l2) -> - let oevar = if ogname = "" then Id.to_string n else ogname in - nevar_to_oevar := CString.Map.add (Id.to_string n2) oevar !nevar_to_oevar; + let oevar = if ogname = "" then Id.to_string n.CAst.v else ogname in + nevar_to_oevar := CString.Map.add (Id.to_string n2.CAst.v) oevar !nevar_to_oevar; iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 | CEvar (n,l), nt' -> (* pass down the old goal evar name *) - match_goals_r (Id.to_string n) nt' nt' + match_goals_r (Id.to_string n.CAst.v) nt' nt' | CSort s, CSort s2 -> () | CCast (c,c'), CCast (c2,c'2) -> constr_expr ogname c c2; @@ -660,3 +663,22 @@ let make_goal_map op np = let ng_to_og = make_goal_map_i op np in (*db_goal_map op np ng_to_og;*) ng_to_og + +let diff_proofs ~diff_opt ?old proof = + let pp_proof p = + let sigma, env = Proof.get_proof_context p in + let pprf = Proof.partial_proof p in + Pp.prlist_with_sep Pp.fnl (pr_econstr_env env sigma) pprf in + match diff_opt with + | DiffOff -> pp_proof proof + | _ -> begin + try + let n_pp = pp_proof proof in + let o_pp = match old with + | None -> Pp.mt() + | Some old -> pp_proof old in + let show_removed = Some (diff_opt = DiffRemoved) in + Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp + with + | Pp_diff.Diff_Failure msg -> Pp.str msg + end diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index ea64439456..6bdd7004fb 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -25,6 +25,10 @@ val write_color_enabled : bool -> unit (** true indicates that color output is enabled *) val color_enabled : unit -> bool +type diffOpt = DiffOff | DiffOn | DiffRemoved + +val string_to_diffs : string -> diffOpt + open Evd open Environ open Constr @@ -84,3 +88,5 @@ type hyp_info = { } val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list + +val diff_proofs : diff_opt:diffOpt -> ?old:Proof.t -> Proof.t -> Pp.t |