Skip to content

Commit

Permalink
fix but with pasting not trimming leading whitespace
Browse files Browse the repository at this point in the history
  • Loading branch information
disconcision committed Feb 7, 2025
1 parent 1b674d5 commit 4acb18d
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 7 deletions.
13 changes: 7 additions & 6 deletions src/haz3lcore/ClipboardCache.re
Original file line number Diff line number Diff line change
Expand Up @@ -17,16 +17,17 @@ let set = (seg: option(Segment.t), str: string): unit =>
let intersection = (ids1: list(Id.t), ids2: list(Id.t)): list(Id.t) =>
List.filter(id => List.mem(id, ids2), ids1);

let get = (pasted: string): Action.t =>
let get = (pasted: string): Action.t => {
/* Note the trimming of leading whitespace on each line */
let trim = Util.StringUtil.trim_leading;
let trimmed_pasted = trim(pasted);
switch (cache^) {
| None => Paste(String(pasted))
| None => Paste(String(trimmed_pasted))
| Some((cached, segment)) =>
let trim = Util.StringUtil.trim_leading;
/* Note the trim */
let trimmed_pasted = trim(pasted);
/* Note that we must replace unique ids here if we want to
* support copying and/or multiples pastes for a copy */
trim(cached) == trimmed_pasted
? Paste(Segment(Segment.IDs.replace(segment)))
: Paste(String(trimmed_pasted));
: Paste(String(trimmed_pasted))
};
};
6 changes: 5 additions & 1 deletion src/util/StringUtil.re
Original file line number Diff line number Diff line change
Expand Up @@ -67,4 +67,8 @@ let escape_linebreaks: string => string =
let unescape_linebreaks: string => string =
Re.Str.global_replace(Re.Str.regexp("\\\\n"), "\n");

let trim_leading = Re.Str.global_replace(Re.Str.regexp("\n[ ]*"), "\n");
let trim_leading = (s: string): string => {
s
|> Re.Str.global_replace(Re.Str.regexp("^[ ]*"), "") // Remove leading spaces at start
|> Re.Str.global_replace(Re.Str.regexp("\n[ ]*"), "\n"); // Remove leading spaces after newlines
};

0 comments on commit 4acb18d

Please sign in to comment.