add lisp packages

2020-12-05 21:29:49 +01:00
parent 85e20365ae
commit a6e2395755
7272 changed files with 1363243 additions and 0 deletions
--- a/lisp/emacs-application-framework/app/terminal/index.html
+++ b/lisp/emacs-application-framework/app/terminal/index.html
@@ -0,0 +1,151 @@
+<!DOCTYPE html>
+<html>
+    <head>
+        <meta charset="utf-8" />
+        <script type="text/javascript" src="%2/node_modules/xterm/lib/xterm.js"></script>
+        <script type="text/javascript" src="%2/node_modules/xterm-addon-attach/lib/xterm-addon-attach.js"></script>
+        <script type="text/javascript" src="%2/node_modules/xterm-addon-fit/lib/xterm-addon-fit.js"></script>
+        <script type="text/javascript" src="%2/node_modules/xterm-addon-search/lib/xterm-addon-search.js"></script>
+        <script type="text/javascript" src="%2/node_modules/xterm-addon-web-links/lib/xterm-addon-web-links.js"></script>
+        <script type="text/javascript" src="%2/%3_theme.js"></script>
+        <link rel="stylesheet" href="%2/node_modules/xterm/css/xterm.css" />
+
+        <style>
+         /* Make terminal fit full area of window */
+         html, body, #xterm, .xterm-screen, canvas {
+             width: 100%;
+             height: 100%;
+             padding: 0;
+             margin: 0;
+         }
+
+         .xterm-viewport {
+             display: none;
+         }
+
+         /* Hide scrollbar */
+         .xterm-viewport {
+             overflow: hidden !important;
+         }
+        </style>
+    </head>
+    <body>
+        <div id="xterm" class="xterm"/>
+
+        <script>
+         try {
+             var socket = new WebSocket("ws://127.0.0.1:%1");
+         }
+         catch(err) {
+             setTimeout('location.reload();',1000);
+         }
+         const term = new Terminal({
+             fontSize: "%4",
+             cursorBlink: true,
+             theme: theme
+         });
+         
+         var title = "%5"
+         
+         const searchAddon = new SearchAddon.SearchAddon();
+
+         function get_selection() {
+             return term.getSelection();
+         }
+
+         function paste(text) {
+             term.paste(text);
+         }
+
+         function scroll_line(number) {
+             term.scrollLines(number);
+         }
+
+         function scroll_page(number) {
+             term.scrollPages(number);
+         }
+
+         function scroll_to_begin() {
+             term.scrollToTop();
+         }
+
+         function scroll_to_bottom() {
+             term.scrollToBottom();
+         }
+
+         function select_all() {
+             term.selectAll();
+         }
+
+         function clear_selection() {
+             term.clearSelection();
+         }
+
+         function find_next(text) {
+             searchAddon.findNext(text);
+         }
+
+         function find_prev(text) {
+             searchAddon.findPrevious(text);
+         }
+
+         socket.onopen = () => {
+             const attachAddon = new AttachAddon.AttachAddon(socket);
+             const fitAddon = new FitAddon.FitAddon();
+             term.loadAddon(attachAddon);
+             term.loadAddon(fitAddon);
+             term.loadAddon(searchAddon);
+             term.loadAddon(new WebLinksAddon.WebLinksAddon());
+             term.open(document.getElementById('xterm'));
+             fitAddon.fit();
+             term.focus();
+
+             setTimeout(() => {
+                 sendSizeToServer();
+             }, 50);
+
+             function sendSizeToServer() {
+                 /* After window resize, make terminal fit before get term size */
+                 fitAddon.fit()
+
+                 let cols = term.cols.toString();
+                 let rows = term.rows.toString();
+                 while (cols.length < 3) {
+                     cols = "0"+cols;
+                 }
+                 while (rows.length < 3) {
+                     rows = "0"+rows;
+                 }
+
+                 console.log("ESCAPED|-- RESIZE:"+cols+";"+rows);
+
+                 socket.send("ESCAPED|-- RESIZE:"+cols+";"+rows);
+             }
+
+             window.addEventListener("resize", sendSizeToServer);
+         }
+
+         socket.onmessage = (msg) => {
+             var re = /:([^\x07].*?)\x07/g;
+             arr = re.exec(msg.data)
+             if(arr) {
+                 if (arr[1] === "/") {
+                     title = arr[1];
+                 }
+                 else {
+                     title = arr[1]+"/"
+                 }
+             }
+            
+             if(msg === "Closing") {
+                 socket.close();
+             }
+         }
+
+         socket.onclose = () => {
+             window.close();
+         }
+         socket.onerror = () => {}
+        </script>
+    </body>
+</html>