frontend: Make buttons nicer

internal/component/static/dist/control/index.html

@@ -1 +1 @@
-<link rel="stylesheet" href="/static/control/index.a0bd71f2.css"><script type="module" src="/static/control/index.a27ed337.js"></script>
+<link rel="stylesheet" href="/static/control/index.b3c7c0f7.css"><script type="module" src="/static/control/index.dbb01556.js"></script>

internal/component/static/dist/control/instance.html

@@ -1 +1 @@
-<link rel="stylesheet" href="/static/control/index.a0bd71f2.css"><script type="module" src="/static/control/index.a27ed337.js"></script>
+<link rel="stylesheet" href="/static/control/index.b3c7c0f7.css"><script type="module" src="/static/control/index.dbb01556.js"></script>

internal/component/static/dist/home/index.d87c909c.js

@@ -0,0 +1 @@
+const e=e=>{const n=document.getElementsByTagName("h"+e);Array.from(n).forEach((e=>{void 0!==e.id&&""!==e.id&&e.appendChild((e=>{const n=document.createElement("a");return n.className="header-link",n.href="#"+e,n.innerHTML="#",n})(e.id))}))};new Array(6).fill(0).forEach(((n,r)=>e(r+1)));

internal/component/static/dist/home/index.html

@@ -1 +1 @@
-<link rel="stylesheet" href="/static/control/index.a0bd71f2.css"><script type="module" src="/static/home/index.38d394c2.js"></script>
+<link rel="stylesheet" href="/static/control/index.b3c7c0f7.css"><script type="module" src="/static/home/index.d87c909c.js"></script>

internal/component/static/src/base/index.css

@@ -1,7 +1,10 @@
 body {
     font-family: system-ui, "Segoe UI", Roboto, Helvetica, Arial, sans-serif, "Apple Color Emoji", "Segoe UI Emoji", "Segoe UI Symbol";
 }
-header, main, footer {
+
+header,
+main,
+footer {
     margin: 2em;
 }
 
@@ -10,20 +13,21 @@ header, main, footer {
 }
 
 .overflow {
-    overflow-x:auto;
+    overflow-x: auto;
 }
 
 .overflow table {
     width: 100%;
 }
 
-.overflow table td:not(:last-child), 
+.overflow table td:not(:last-child),
 .overflow table th:not(:last-child) {
-    width:1px;
-    text-align:left;
+    width: 1px;
+    text-align: left;
     white-space: nowrap;
 }
-.overflow table td:last-child, 
+
+.overflow table td:last-child,
 .overflow table th:last-child {
     white-space: nowrap;
 }
@@ -31,4 +35,11 @@ header, main, footer {
 .hspace {
     display: block;
     height: 2em;
+}
+
+.pure-button-action {
+    background-color: rgb(66, 184, 221) !important;
+}
+.pure-button-success {
+    background-color: rgb(28, 184, 65) !important;
 }

internal/component/static/src/entry/control/index.css

@@ -1,5 +1,15 @@
 .wisski {
-    padding-left: 5px;
+    padding: 1em;
+}
+
+.wisski h3 {
+    padding: 0;
+}
+
+.wisski a.pure-button {
+    float: right;
+    position: relative;
+    bottom: 1em;
 }
 
 .wisski.running {

internal/component/static/src/lib/autolink/index.css

@@ -17,5 +17,6 @@ h3:hover .header-link,
 h4:hover .header-link,
 h5:hover .header-link,
 h6:hover .header-link {
+    color: black !important;
     opacity: 1;
 }

internal/component/static/src/lib/autolink/index.ts

@@ -1,7 +1,7 @@
 import "./index.css"
 
 /** Adapted from http://blog.parkermoore.de/2014/08/01/header-anchor-links-in-vanilla-javascript-for-github-pages-and-jekyll/ */
-const anchorForId = (id) => {
+const anchorForId = (id: string) => {
     const anchor = document.createElement("a")
     anchor.className = "header-link"
     anchor.href = "#" + id
@@ -9,7 +9,7 @@ const anchorForId = (id) => {
     return anchor
 }
 
-const linkifyAnchors = (level) => {
+const linkifyAnchors = (level: number) => {
     const headers = document.getElementsByTagName("h" + level);
     Array.from(headers).forEach((header) => {
         if (typeof header.id === "undefined" || header.id === "") return

internal/component/static/src/lib/remote/index.ts

@@ -71,12 +71,15 @@ Array.from(elements).forEach((element) => {
         
         // create a button to eventually close everything
         const button = document.createElement("button")
-        button.className = "pure-button"
+        button.className = "pure-button pure-button-success"
         button.append("Close")
         button.addEventListener('click', function (event) {
             event.preventDefault();
             modal.parentNode?.removeChild(modal);
         })
+        
+        const onbeforeunload = window.onbeforeunload;
+        window.onbeforeunload = () => "A remote session is in progress. Are you sure you want to leave?";
 
         // when closing, add a button to the modal!
         let didClose = false
@@ -84,6 +87,7 @@ Array.from(elements).forEach((element) => {
             if (didClose) return
             didClose = true
 
+            window.onbeforeunload = onbeforeunload;
             modal.append(button)
             // DEBUG: print terminal stats!
             // const quota = (println.paintedFrames / (println.missedFrames + println.paintedFrames)) * 100