aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/class.ml13
-rw-r--r--vernac/record.ml14
-rw-r--r--vernac/topfmt.ml124
3 files changed, 96 insertions, 55 deletions
diff --git a/vernac/class.ml b/vernac/class.ml
index e425e6474d..614b2181d9 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -73,7 +73,7 @@ let check_reference_arity ref =
let check_arity = function
| CL_FUN | CL_SORT -> ()
| CL_CONST cst -> check_reference_arity (ConstRef cst)
- | CL_PROJ cst -> check_reference_arity (ConstRef cst)
+ | CL_PROJ p -> check_reference_arity (ConstRef (Projection.Repr.constant p))
| CL_SECVAR id -> check_reference_arity (VarRef id)
| CL_IND kn -> check_reference_arity (IndRef kn)
@@ -92,8 +92,8 @@ let uniform_cond sigma ctx lt =
let class_of_global = function
| ConstRef sp ->
- if Environ.is_projection sp (Global.env ())
- then CL_PROJ sp else CL_CONST sp
+ (match Recordops.find_primitive_projection sp with
+ | Some p -> CL_PROJ p | None -> CL_CONST sp)
| IndRef sp -> CL_IND sp
| VarRef id -> CL_SECVAR id
| ConstructRef _ as c ->
@@ -143,8 +143,8 @@ let get_target t ind =
CL_FUN
else
match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
- | CL_CONST p when Environ.is_projection p (Global.env ()) ->
- CL_PROJ p
+ | CL_CONST p when Recordops.is_primitive_projection p ->
+ CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
| x -> x
let strength_of_cl = function
@@ -165,7 +165,8 @@ let get_strength stre ref cls clt =
let ident_key_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
- | CL_CONST sp | CL_PROJ sp -> Label.to_string (Constant.label sp)
+ | CL_CONST sp -> Label.to_string (Constant.label sp)
+ | CL_PROJ sp -> Label.to_string (Projection.Repr.label sp)
| CL_IND (sp,_) -> Label.to_string (MutInd.label sp)
| CL_SECVAR id -> Id.to_string id
diff --git a/vernac/record.ml b/vernac/record.ml
index 7a8ce7d25a..6b5c538df2 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -324,12 +324,16 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
| Name fid -> try
let kn, term =
if is_local_assum decl && primitive then
- (** Already defined in the kernel silently *)
- let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
- let kn = destConstRef gr in
+ let p = Projection.Repr.make indsp
+ ~proj_npars:mib.mind_nparams
+ ~proj_arg:i
+ (Label.of_id fid)
+ in
+ (** Already defined by declare_mind silently *)
+ let kn = Projection.Repr.constant p in
Declare.definition_message fid;
- UnivNames.register_universe_binders gr ubinders;
- kn, mkProj (Projection.make kn false,mkRel 1)
+ UnivNames.register_universe_binders (ConstRef kn) ubinders;
+ kn, mkProj (Projection.make p false,mkRel 1)
else
let ccl = subst_projection fid subst ti in
let body = match decl with
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 609dac69aa..f842ca5ead 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -181,6 +181,10 @@ let default_tag_map () = let open Terminal in [
; "tactic.keyword" , make ~bold:true ()
; "tactic.primitive" , make ~fg_color:`LIGHT_GREEN ()
; "tactic.string" , make ~fg_color:`LIGHT_RED ()
+ ; "diff.added" , make ~bg_color:(`RGB(0,141,0)) ~underline:true ()
+ ; "diff.removed" , make ~bg_color:(`RGB(170,0,0)) ~underline:true ()
+ ; "diff.added.bg" , make ~bg_color:(`RGB(0,91,0)) ()
+ ; "diff.removed.bg" , make ~bg_color:(`RGB(91,0,0)) ()
]
let tag_map = ref CString.Map.empty
@@ -198,72 +202,103 @@ let parse_color_config file =
let dump_tags () = CString.Map.bindings !tag_map
+let empty = Terminal.make ()
+let default_style = Terminal.reset_style
+
+let get_style tag =
+ try CString.Map.find tag !tag_map
+ with Not_found -> empty;;
+
+let get_open_seq tags =
+ let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in
+ Terminal.eval (Terminal.diff default_style style);;
+
+let get_close_seq tags =
+ let style = List.fold_left (fun a b -> Terminal.merge a (get_style b)) default_style tags in
+ Terminal.eval (Terminal.diff style default_style);;
+
+let diff_tag_stack = ref [] (* global, just like std_ft *)
+
(** Not thread-safe. We should put a lock somewhere if we print from
different threads. Do we? *)
let make_style_stack () =
(** Default tag is to reset everything *)
- let empty = Terminal.make () in
- let default_tag = Terminal.({
- fg_color = Some `DEFAULT;
- bg_color = Some `DEFAULT;
- bold = Some false;
- italic = Some false;
- underline = Some false;
- negative = Some false;
- prefix = None;
- suffix = None;
- })
- in
let style_stack = ref [] in
let peek () = match !style_stack with
- | [] -> default_tag (** Anomalous case, but for robustness *)
+ | [] -> default_style (** Anomalous case, but for robustness *)
| st :: _ -> st
in
- let push tag =
- let style =
- try CString.Map.find tag !tag_map
- with | Not_found -> empty
- in
- (** Use the merging of the latest tag and the one being currently pushed.
- This may be useful if for instance the latest tag changes the background and
- the current one the foreground, so that the two effects are additioned. *)
+ let open_tag tag =
+ let (tpfx, ttag) = split_tag tag in
+ if tpfx = end_pfx then "" else
+ let style = get_style ttag in
+ (** Merge the current settings and the style being pushed. This allows
+ restoring the previous settings correctly in a pop when both set the same
+ attribute. Example: current settings have red FG, the pushed style has
+ green FG. When popping the style, we should set red FG, not default FG. *)
let style = Terminal.merge (peek ()) style in
+ let diff = Terminal.diff (peek ()) style in
style_stack := style :: !style_stack;
- Terminal.eval style
+ if tpfx = start_pfx then diff_tag_stack := ttag :: !diff_tag_stack;
+ Terminal.eval diff
in
- let pop _ = match !style_stack with
- | [] -> (** Something went wrong, we fallback *)
- Terminal.eval default_tag
- | _ :: rem -> style_stack := rem;
- Terminal.eval (peek ())
+ let close_tag tag =
+ let (tpfx, _) = split_tag tag in
+ if tpfx = start_pfx then "" else begin
+ if tpfx = end_pfx then diff_tag_stack := (try List.tl !diff_tag_stack with tl -> []);
+ match !style_stack with
+ | [] -> (** Something went wrong, we fallback *)
+ Terminal.eval default_style
+ | cur :: rem -> style_stack := rem;
+ if cur = (peek ()) then "" else
+ if rem = [] then Terminal.reset else
+ Terminal.eval (Terminal.diff cur (peek ()))
+ end
in
let clear () = style_stack := [] in
- push, pop, clear
+ open_tag, close_tag, clear
let make_printing_functions () =
- let empty = Terminal.make () in
let print_prefix ft tag =
- let style =
- try CString.Map.find tag !tag_map
- with | Not_found -> empty
- in
- match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> ()
- in
+ let (tpfx, ttag) = split_tag tag in
+ if tpfx <> end_pfx then
+ let style = get_style ttag in
+ match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () in
+
let print_suffix ft tag =
- let style =
- try CString.Map.find tag !tag_map
- with | Not_found -> empty
- in
- match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> ()
- in
+ let (tpfx, ttag) = split_tag tag in
+ if tpfx <> start_pfx then
+ let style = get_style ttag in
+ match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () in
+
print_prefix, print_suffix
+let init_output_fns () =
+ let reopen_highlight = ref "" in
+ let open Format in
+ let fns = Format.pp_get_formatter_out_functions !std_ft () in
+ let newline () =
+ if !diff_tag_stack <> [] then begin
+ let close = get_close_seq !diff_tag_stack in
+ fns.out_string close 0 (String.length close);
+ reopen_highlight := get_open_seq (List.rev !diff_tag_stack);
+ end;
+ fns.out_string "\n" 0 1 in
+ let string s off n =
+ if !reopen_highlight <> "" && String.trim (String.sub s off n) <> "" then begin
+ fns.out_string !reopen_highlight 0 (String.length !reopen_highlight);
+ reopen_highlight := ""
+ end;
+ fns.out_string s off n in
+ let new_fns = { fns with out_string = string; out_newline = newline } in
+ Format.pp_set_formatter_out_functions !std_ft new_fns;;
+
let init_terminal_output ~color =
- let push_tag, pop_tag, clear_tag = make_style_stack () in
+ let open_tag, close_tag, clear_tag = make_style_stack () in
let print_prefix, print_suffix = make_printing_functions () in
let tag_handler ft = {
- Format.mark_open_tag = push_tag;
- Format.mark_close_tag = pop_tag;
+ Format.mark_open_tag = open_tag;
+ Format.mark_close_tag = close_tag;
Format.print_open_tag = print_prefix ft;
Format.print_close_tag = print_suffix ft;
} in
@@ -271,6 +306,7 @@ let init_terminal_output ~color =
(* Use 0-length markers *)
begin
std_logger_cleanup := clear_tag;
+ init_output_fns ();
Format.pp_set_mark_tags !std_ft true;
Format.pp_set_mark_tags !err_ft true
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 15:51:18 +0000