Improve selection of paste content

[cgzones]

When selecting the content of a paste either via Ctrl-a or via mouse selection extra newlines are included.

E.g. with a paste of

test
test1
test2
test3
test4
test5

Ctrl-a results on chromium in

home
download raw
test
test1
test2
test3
test4
test5

and on firefox in

test

test1

test2

test3

test4

test5

Selecting the content via mouse works on chromium, but on Firefox the result is

test

test1

test2

test3

test4

test5

[matze]

It's hard. We could do things like intercepting Ctrl-C, using the selection and manually insert the massaged text into the clipboard but … not sure if that is super portable. I'll keep it open and up for grabs.

[cgzones]

With the following patch I got it to work on chromium, but firefox still includes two newlines at the start and at the end:

diff --git a/src/highlight.rs b/src/highlight.rs
index 99fe0a2..e2a78fd 100644
--- a/src/highlight.rs
+++ b/src/highlight.rs
@@ -109,9 +109,13 @@ fn highlight(source: &str, ext: &str) -> Result<String, Error> {
             html.push_str(&"<span>".repeat(delta.abs().try_into()?));
         }
 
-        // Strip stray newlines that cause vertically stretched lines.
-        for c in formatted.chars().filter(|c| *c != '\n') {
-            html.push(c);
+        if delta == 0 && formatted.is_empty() {
+            html.push_str(r#"<span class="text plain">\r</span>"#);
+        } else {
+            // Strip stray newlines that cause vertically stretched lines.
+            for c in formatted.chars().filter(|c| *c != '\n' /*&& *c != '\r'*/) {
+                html.push(c);
+            }
         }
 
         if delta > 0 {
diff --git a/src/themes/style.css b/src/themes/style.css
index f90cbca..0c162fa 100644
--- a/src/themes/style.css
+++ b/src/themes/style.css
@@ -52,6 +52,7 @@ header {
   justify-content: flex-end;
   align-items: center;
   padding: 0 1em 0 1em;
+  user-select: none;
 }
 
 content {
@@ -303,6 +304,7 @@ td.line-number {
 .line {
   word-wrap: normal;
   white-space: pre;
+  user-select: text;
 }
 
 .center {