aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/.merlin.in (renamed from ide/.merlin)0
-rw-r--r--ide/MacOS/default_accel_map1
-rw-r--r--ide/coq.ml47
-rw-r--r--ide/coq.mli10
-rw-r--r--ide/coq_commands.ml1
-rw-r--r--ide/coq_lex.mll6
-rw-r--r--ide/coqide.ml29
-rw-r--r--ide/coqide_ui.ml4
-rw-r--r--ide/gtk_parsing.ml7
-rw-r--r--ide/idetop.ml36
-rw-r--r--ide/ideutils.ml43
-rw-r--r--ide/preferences.ml28
-rw-r--r--ide/preferences.mli2
-rw-r--r--ide/wg_ProofView.ml4
14 files changed, 173 insertions, 45 deletions
diff --git a/ide/.merlin b/ide/.merlin.in
index 953b5dce4c..953b5dce4c 100644
--- a/ide/.merlin
+++ b/ide/.merlin.in
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
index 47612cdf72..54a592a04d 100644
--- a/ide/MacOS/default_accel_map
+++ b/ide/MacOS/default_accel_map
@@ -217,7 +217,6 @@
; (gtk_accel_path "<Actions>/Tactics/Tactic casetype" "")
; (gtk_accel_path "<Actions>/Tactics/Tactic cbv in" "")
; (gtk_accel_path "<Actions>/Templates/Template Load" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fourier" "")
; (gtk_accel_path "<Actions>/Templates/Template Goal" "")
; (gtk_accel_path "<Actions>/Tactics/Tactic exists" "")
; (gtk_accel_path "<Actions>/Tactics/Tactic decompose record" "")
diff --git a/ide/coq.ml b/ide/coq.ml
index 63986935aa..e948360191 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -530,20 +530,31 @@ let break_coqtop coqtop workers =
module PrintOpt =
struct
- type t = string list
+ type _ t =
+ | BoolOpt : string list -> bool t
+ | StringOpt : string list -> string t
+
+ let opt_name (type a) : a t -> string list = function
+ | BoolOpt l -> l
+ | StringOpt l -> l
+
+ let opt_data (type a) (key : a t) (v : a) = match key with
+ | BoolOpt l -> Interface.BoolValue v
+ | StringOpt l -> Interface.StringValue v
(* Boolean options *)
- let implicit = ["Printing"; "Implicit"]
- let coercions = ["Printing"; "Coercions"]
- let raw_matching = ["Printing"; "Matching"]
- let notations = ["Printing"; "Notations"]
- let all_basic = ["Printing"; "All"]
- let existential = ["Printing"; "Existential"; "Instances"]
- let universes = ["Printing"; "Universes"]
- let unfocused = ["Printing"; "Unfocused"]
+ let implicit = BoolOpt ["Printing"; "Implicit"]
+ let coercions = BoolOpt ["Printing"; "Coercions"]
+ let raw_matching = BoolOpt ["Printing"; "Matching"]
+ let notations = BoolOpt ["Printing"; "Notations"]
+ let all_basic = BoolOpt ["Printing"; "All"]
+ let existential = BoolOpt ["Printing"; "Existential"; "Instances"]
+ let universes = BoolOpt ["Printing"; "Universes"]
+ let unfocused = BoolOpt ["Printing"; "Unfocused"]
+ let diff = StringOpt ["Diffs"]
- type bool_descr = { opts : t list; init : bool; label : string }
+ type 'a descr = { opts : 'a t list; init : 'a; label : string }
let bool_items = [
{ opts = [implicit]; init = false; label = "Display _implicit arguments" };
@@ -561,24 +572,32 @@ struct
{ opts = [unfocused]; init = false; label = "Display _unfocused goals" }
]
+ let diff_item = { opts = [diff]; init = "off"; label = "Display _proof diffs" }
+
(** The current status of the boolean options *)
let current_state = Hashtbl.create 11
- let set opt v = Hashtbl.replace current_state opt v
+ let set (type a) (opt : a t) (v : a) =
+ Hashtbl.replace current_state (opt_name opt) (opt_data opt v)
let reset () =
let init_descr d = List.iter (fun o -> set o d.init) d.opts in
- List.iter init_descr bool_items
+ List.iter init_descr bool_items;
+ List.iter (fun o -> set o diff_item.init) diff_item.opts
let _ = reset ()
- let printing_unfocused () = Hashtbl.find current_state unfocused
+ let printing_unfocused () =
+ let BoolOpt unfocused = unfocused in
+ match Hashtbl.find current_state unfocused with
+ | Interface.BoolValue b -> b
+ | _ -> assert false
(** Transmitting options to coqtop *)
let enforce h k =
- let mkopt o v acc = (o, Interface.BoolValue v) :: acc in
+ let mkopt o v acc = (o, v) :: acc in
let opts = Hashtbl.fold mkopt current_state [] in
eval_call (Xmlprotocol.set_options opts) h
(function
diff --git a/ide/coq.mli b/ide/coq.mli
index 40a6dea8d3..3af0aa697e 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -134,13 +134,15 @@ val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query
module PrintOpt :
sig
- type t (** Representation of an option *)
+ type 'a t (** Representation of an option *)
- type bool_descr = { opts : t list; init : bool; label : string }
+ type 'a descr = { opts : 'a t list; init : 'a; label : string }
- val bool_items : bool_descr list
+ val bool_items : bool descr list
- val set : t -> bool -> unit
+ val diff_item : string descr
+
+ val set : 'a t -> 'a -> unit
val printing_unfocused: unit -> bool
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index f5dba2085a..b0bafb7930 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -311,7 +311,6 @@ let tactics =
"fix __ with";
"fold";
"fold __ in";
- "fourier";
"functional induction";
];
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 1fdd7317b5..b6654f6d7a 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -23,7 +23,11 @@ let number = [ '0'-'9' ]+
let string = "\"" _+ "\""
-let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
+let alpha = ['a'-'z' 'A'-'Z']
+
+let ident = alpha (alpha | number | '_' | "'")*
+
+let undotted_sep = ((number | '[' ident ']') space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
let vernac_control = "Fail" | "Time" | "Redirect" space+ string | "Timeout" space+ number
diff --git a/ide/coqide.ml b/ide/coqide.ml
index aa816f2b8b..00d43e6e64 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -826,6 +826,7 @@ let refresh_notebook_pos () =
let menu = GAction.add_actions
let item = GAction.add_action
+let radio = GAction.add_radio_action
(** Toggle items in menus for printing options *)
@@ -1043,7 +1044,27 @@ let build_ui () =
~callback:(fun _ -> show_toolbar#set (not show_toolbar#get));
item "Query Pane" ~label:"_Query Pane"
~accel:"F1"
- ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane)
+ ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane);
+ GAction.group_radio_actions
+ ~init_value:(
+ let v = diffs#get in
+ List.iter (fun o -> Opt.set o v) Opt.diff_item.Opt.opts;
+ if v = "on" then 1
+ else if v = "removed" then 2
+ else 0)
+ ~callback:begin fun n ->
+ (match n with
+ | 0 -> List.iter (fun o -> Opt.set o "off"; diffs#set "off") Opt.diff_item.Opt.opts
+ | 1 -> List.iter (fun o -> Opt.set o "on"; diffs#set "on") Opt.diff_item.Opt.opts
+ | 2 -> List.iter (fun o -> Opt.set o "removed"; diffs#set "removed") Opt.diff_item.Opt.opts
+ | _ -> assert false);
+ send_to_coq (fun sn -> sn.coqops#show_goals)
+ end
+ [
+ radio "Unset diff" 0 ~label:"_Don't show diffs";
+ radio "Set diff" 1 ~label:"Show diffs: only _added";
+ radio "Set removed diff" 2 ~label:"Show diffs: added and _removed";
+ ];
];
toggle_items view_menu Coq.PrintOpt.bool_items;
@@ -1106,15 +1127,15 @@ let build_ui () =
];
alpha_items templates_menu "Template" Coq_commands.commands;
- let qitem s sc ?(dots = true) =
- let query = if dots then s ^ "..." else s in
+ let qitem s sc =
+ let query = s ^ "..." in
item s ~label:("_"^s)
~accel:(modifier_for_queries#get^sc)
~callback:(Query.query query)
in
menu queries_menu [
item "Queries" ~label:"_Queries";
- qitem "Search" "K" ~dots:false;
+ qitem "Search" "K";
qitem "Check" "C";
qitem "Print" "P";
qitem "About" "A";
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 717c4000f5..91c529932f 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -86,6 +86,10 @@ let init () =
\n <menuitem action='Display universe levels' />\
\n <menuitem action='Display all low-level contents' />\
\n <menuitem action='Display unfocused goals' />\
+\n <separator/>\
+\n <menuitem action='Unset diff' />\
+\n <menuitem action='Set diff' />\
+\n <menuitem action='Set removed diff' />\
\n </menu>\
\n <menu action='Navigation'>\
\n <menuitem action='Forward' />\
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 9f5c992444..d554bebdd3 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -35,8 +35,11 @@ let find_word_start (it:GText.iter) =
(Minilib.log "find_word_start: cannot backward"; it)
else if is_word_char it#char
then step_to_start it
- else (it#nocopy#forward_char;
- Minilib.log ("Word start at: "^(string_of_int it#offset));it)
+ else begin
+ ignore(it#nocopy#forward_char);
+ Minilib.log ("Word start at: "^(string_of_int it#offset));
+ it
+ end
in
step_to_start it#copy
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7abbf239b2..d846b3abb5 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -53,10 +53,12 @@ let coqide_known_option table = List.mem table [
["Printing";"Records"];
["Printing";"Existential";"Instances"];
["Printing";"Universes"];
- ["Printing";"Unfocused"]]
+ ["Printing";"Unfocused"];
+ ["Diffs"]]
let is_known_option cmd = match Vernacprop.under_control cmd with
| VernacSetOption (_, o, BoolValue true)
+ | VernacSetOption (_, o, StringValue _)
| VernacUnsetOption (_, o) -> coqide_known_option o
| _ -> false
@@ -80,7 +82,7 @@ let set_doc doc = ide_doc := Some doc
let add ((s,eid),(sid,verbose)) =
let doc = get_doc () in
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+ let pa = Pcoq.Parsable.make (Stream.of_string s) in
let loc_ast = Stm.parse_sentence ~doc sid pa in
let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
set_doc doc;
@@ -113,14 +115,14 @@ let edit_at id =
* be removed in the next version of the protocol.
*)
let query (route, (s,id)) =
- let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+ let pa = Pcoq.Parsable.make (Stream.of_string s) in
let doc = get_doc () in
Stm.query ~at:id ~doc ~route pa
let annotate phrase =
let doc = get_doc () in
let {CAst.loc;v=ast} =
- let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
+ let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
in
(* XXX: Width should be a parameter of annotate... *)
@@ -151,7 +153,7 @@ let hyp_next_tac sigma env decl =
("inversion clear "^id_s), ("inversion_clear "^id_s^".")
]
-let concl_next_tac sigma concl =
+let concl_next_tac =
let expand s = (s,s^".") in
List.map expand ([
"intro";
@@ -202,13 +204,28 @@ let export_pre_goals pgs =
Interface.given_up_goals = pgs.Proof.given_up_goals
}
+let add_diffs oldp newp intf =
+ let open Interface in
+ let (hyps_pp_list, concl_pp) = Proof_diffs.diff_first_goal oldp newp in
+ match intf.fg_goals with
+ | [] -> intf
+ | first_goal :: tl ->
+ { intf with fg_goals = { first_goal with goal_hyp = hyps_pp_list; goal_ccl = concl_pp } :: tl }
+
let goals () =
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
try
- let pfts = Proof_global.give_me_the_proof () in
- Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
- with Proof_global.NoCurrentProof -> None
+ let newp = Proof_global.give_me_the_proof () in
+ let intf = export_pre_goals (Proof.map_structured_proof newp process_goal) in
+ if Proof_diffs.show_diffs () then
+ let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
+ try
+ Some (add_diffs oldp (Some newp) intf)
+ with Pp_diff.Diff_Failure _ -> Some intf
+ else
+ Some intf
+ with Proof_global.NoCurrentProof -> None;;
let evars () =
try
@@ -230,10 +247,9 @@ let hints () =
| [] -> None
| g :: _ ->
let env = Goal.V82.env sigma g in
- let hint_goal = concl_next_tac sigma g in
let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
- Some (hint_hyps, hint_goal)
+ Some (hint_hyps, concl_next_tac)
with Proof_global.NoCurrentProof -> None
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index e96b992999..960beb8455 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -37,6 +37,11 @@ let flash_info =
let flash_context = status#new_context ~name:"Flash" in
(fun ?(delay=5000) s -> flash_context#flash ~delay s)
+(* Note: Setting the same attribute with two separate tags appears to use
+the first value applied and not the second. I saw this trying to set the background
+color on Windows. A clean fix, if ever needed, would be to combine the attributes
+of the tags into a single composite tag before applying. This is left as an
+exercise for the reader. *)
let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
(** FIXME: LablGTK2 does not export the C insert_with_tags function, so that
it has to reimplement its own helper function. Unluckily, it relies on
@@ -50,21 +55,51 @@ let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
let start = buf#get_iter_at_mark mark in
let stop = buf#get_iter_at_mark rmark in
let iter tag = buf#apply_tag tag ~start ~stop in
- List.iter iter tags
+ List.iter iter (List.rev tags)
+
+let nl_white_regex = Str.regexp "^\\( *\n *\\)"
+let diff_regex = Str.regexp "^diff."
let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg =
let open Xml_datatype in
+ let dtags = ref [] in
let tag name =
match GtkText.TagTable.lookup buf#tag_table name with
| None -> raise Not_found
| Some tag -> new GText.tag tag
in
let rmark = `MARK (buf#create_mark buf#start_iter) in
+ (* insert the string, but don't apply diff highlights to white space at the begin/end of line *)
+ let rec insert_str tags s =
+ try
+ let _ = Str.search_forward nl_white_regex s 0 in
+ insert_with_tags buf mark rmark tags (Str.matched_group 1 s);
+ let mend = Str.match_end () in
+ insert_str tags (String.sub s mend (String.length s - mend))
+ with Not_found -> begin
+ let etags = try List.hd !dtags :: tags with hd -> tags in
+ insert_with_tags buf mark rmark etags s
+ end
+ in
let rec insert tags = function
- | PCData s -> insert_with_tags buf mark rmark tags s
+ | PCData s -> insert_str tags s
| Element (t, _, children) ->
- let tags = try tag t :: tags with Not_found -> tags in
- List.iter (fun xml -> insert tags xml) children
+ let (pfx, tname) = Pp.split_tag t in
+ let is_diff = try let _ = Str.search_forward diff_regex tname 0 in true with Not_found -> false in
+ let (tags, have_tag) =
+ try
+ let t = tag tname in
+ if is_diff && pfx <> Pp.end_pfx then
+ dtags := t :: !dtags;
+ if pfx = "" then
+ ((if is_diff then tags else t :: tags), true)
+ else
+ (tags, true)
+ with Not_found -> (tags, false)
+ in
+ List.iter (fun xml -> insert tags xml) children;
+ if have_tag && is_diff && pfx <> Pp.start_pfx then
+ dtags := (try List.tl !dtags with tl -> []);
in
let () = try insert tags msg with _ -> () in
buf#delete_mark rmark
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 11aaf6e8cc..955ee87840 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -25,6 +25,7 @@ type tag = {
tag_bold : bool;
tag_italic : bool;
tag_underline : bool;
+ tag_strikethrough : bool;
}
(** Generic preferences *)
@@ -215,15 +216,17 @@ object
string_of_bool tag.tag_bold;
string_of_bool tag.tag_italic;
string_of_bool tag.tag_underline;
+ string_of_bool tag.tag_strikethrough;
]
method into = function
- | [fg; bg; bd; it; ul] ->
+ | [fg; bg; bd; it; ul; st] ->
(try Some {
tag_fg_color = _to fg;
tag_bg_color = _to bg;
tag_bold = bool_of_string bd;
tag_italic = bool_of_string it;
tag_underline = bool_of_string ul;
+ tag_strikethrough = bool_of_string st;
}
with _ -> None)
| _ -> None
@@ -429,12 +432,13 @@ let tags = ref Util.String.Map.empty
let list_tags () = !tags
-let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) () = {
+let make_tag ?fg ?bg ?(bold = false) ?(italic = false) ?(underline = false) ?(strikethrough = false) () = {
tag_fg_color = fg;
tag_bg_color = bg;
tag_bold = bold;
tag_italic = italic;
tag_underline = underline;
+ tag_strikethrough = strikethrough;
}
let create_tag name default =
@@ -470,6 +474,12 @@ let create_tag name default =
tag#set_property (`UNDERLINE_SET true);
tag#set_property (`UNDERLINE `SINGLE)
end;
+ begin match pref#get.tag_strikethrough with
+ | false -> tag#set_property (`STRIKETHROUGH_SET false)
+ | true ->
+ tag#set_property (`STRIKETHROUGH_SET true);
+ tag#set_property (`STRIKETHROUGH true)
+ end;
in
let iter table =
let tag = GText.tag ~name () in
@@ -480,6 +490,8 @@ let create_tag name default =
List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table];
tags := Util.String.Map.add name pref !tags
+(* note these appear to only set the defaults; they don't override
+the user selection from the Edit/Preferences/Tags dialog *)
let () =
let iter (name, tag) = create_tag name tag in
List.iter iter [
@@ -498,6 +510,10 @@ let () =
("tactic.keyword", make_tag ());
("tactic.primitive", make_tag ());
("tactic.string", make_tag ());
+ ("diff.added", make_tag ~bg:"#b6f1c0" ~underline:true ());
+ ("diff.removed", make_tag ~bg:"#f6b9c1" ~strikethrough:true ());
+ ("diff.added.bg", make_tag ~bg:"#e9feee" ());
+ ("diff.removed.bg", make_tag ~bg:"#fce9eb" ());
]
let processed_color =
@@ -549,6 +565,9 @@ let nanoPG =
let user_queries =
new preference ~name:["user_queries"] ~init:[] ~repr:Repr.(string_pair_list '$')
+let diffs =
+ new preference ~name:["diffs"] ~init:"off" ~repr:Repr.(string)
+
class tag_button (box : Gtk.box Gtk.obj) =
object (self)
@@ -561,6 +580,7 @@ object (self)
val bold = GButton.toggle_button ()
val italic = GButton.toggle_button ()
val underline = GButton.toggle_button ()
+ val strikethrough = GButton.toggle_button ()
method set_tag tag =
let track c but set = match c with
@@ -574,6 +594,7 @@ object (self)
bold#set_active tag.tag_bold;
italic#set_active tag.tag_italic;
underline#set_active tag.tag_underline;
+ strikethrough#set_active tag.tag_strikethrough;
method tag =
let get but set =
@@ -586,6 +607,7 @@ object (self)
tag_bold = bold#active;
tag_italic = italic#active;
tag_underline = underline#active;
+ tag_strikethrough = strikethrough#active;
}
initializer
@@ -599,6 +621,7 @@ object (self)
set_stock bold `BOLD;
set_stock italic `ITALIC;
set_stock underline `UNDERLINE;
+ set_stock strikethrough `STRIKETHROUGH;
box#pack fg_color#coerce;
box#pack fg_unset#coerce;
box#pack bg_color#coerce;
@@ -606,6 +629,7 @@ object (self)
box#pack bold#coerce;
box#pack italic#coerce;
box#pack underline#coerce;
+ box#pack strikethrough#coerce;
let cb but obj = obj#set_sensitive (not but#active) in
let _ = fg_unset#connect#toggled ~callback:(fun () -> cb fg_unset fg_color#misc) in
let _ = bg_unset#connect#toggled ~callback:(fun () -> cb bg_unset bg_color#misc) in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index ccf028aee4..dd2976efc2 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -21,6 +21,7 @@ type tag = {
tag_bold : bool;
tag_italic : bool;
tag_underline : bool;
+ tag_strikethrough : bool;
}
class type ['a] repr =
@@ -101,6 +102,7 @@ val tab_length : int preference
val highlight_current_line : bool preference
val nanoPG : bool preference
val user_queries : (string * string) list preference
+val diffs : string preference
val save_pref : unit -> unit
val load_pref : unit -> unit
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index b3088ee288..9be562d3ed 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -103,7 +103,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat
else []
in
proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt);
- insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal);
+ insert_xml ~tags:[Tags.Proof.goal] proof#buffer (Richpp.richpp_of_pp width cur_goal);
proof#buffer#insert "\n"
in
(* Insert remaining goals (no hypotheses) *)
@@ -128,7 +128,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat
ignore(proof#buffer#place_cursor
~where:(proof#buffer#end_iter#backward_to_tag_toggle
(Some Tags.Proof.goal)));
- ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT)
+ ignore(proof#scroll_to_mark `INSERT)
let rec flatten = function
| [] -> []
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 08:26:15 +0000