copy button

xuwei-k · Mar 10, 2024 · a289f8d · a289f8d
1 parent d660c4c
commit a289f8d
Showing 1 changed file with 19 additions and 0 deletions.
diff --git a/sources/main.js b/sources/main.js
@@ -238,6 +238,25 @@ const App = () => {
             <p></p>
           </div>
           <div class="row">
+            <div class="col">
+              <button
+                class="btn btn-primary"
+                onclick=${() => {
+                  navigator.clipboard.writeText(r.ast);
+                  if (window.getSelection) {
+                    const selection = window.getSelection();
+                    const range = document.createRange();
+                    range.selectNodeContents(
+                      document.getElementById("output_scala"),
+                    );
+                    selection.removeAllRanges();
+                    selection.addRange(range);
+                  }
+                }}
+              >
+                copy
+              </button>
+            </div>
             <div class="col">
               <button
                 class="btn btn-primary"