Patch for CR #325 and code improvement

master
Hollow Man 6 years ago
parent 7536509621
commit 14f16391d3
No known key found for this signature in database
GPG Key ID: 6CA2A0660F48F7A
  1. 10
      app/terminal/buffer.py
  2. 13
      app/terminal/index.html

@ -42,6 +42,7 @@ class AppBuffer(BrowserBuffer):
arguments_dict = json.loads(arguments)
self.command = arguments_dict["command"]
self.start_directory = arguments_dict["directory"]
self.current_directory = self.start_directory
self.index_file = os.path.join(os.path.dirname(__file__), "index.html")
self.server_js = os.path.join(os.path.dirname(__file__), "server.js")
@ -77,12 +78,15 @@ class AppBuffer(BrowserBuffer):
(self.emacs_var_dict["eaf-terminal-dark-mode"] == "" and self.emacs_var_dict["eaf-emacs-theme-mode"] == "dark"):
theme = "dark"
with open(self.index_file, "r") as f:
html = f.read().replace("%1", str(self.port)).replace("%2", "file://" + os.path.join(os.path.dirname(__file__))).replace("%3", theme).replace("%4", self.emacs_var_dict["eaf-terminal-font-size"])
html = f.read().replace("%1", str(self.port)).replace("%2", "file://" + os.path.join(os.path.dirname(__file__))).replace("%3", theme).replace("%4", self.emacs_var_dict["eaf-terminal-font-size"]).replace("%5", self.current_directory)
self.buffer_widget.setHtml(html)
def on_change_directory(self):
self.update_title()
self.eval_in_emacs.emit('''(setq default-directory "'''+self.buffer_widget.execute_js("title")+'''")''')
changed_directory = self.buffer_widget.execute_js("title")
if not str(changed_directory) == self.current_directory:
self.update_title()
self.eval_in_emacs.emit('''(setq default-directory "'''+ str(changed_directory) +'''")''')
self.current_directory = str(changed_directory)
def update_title(self):
self.change_title(self.buffer_widget.execute_js("title"))

@ -45,7 +45,7 @@
theme: theme
});
var title = "~/"
var title = "%5"
const searchAddon = new SearchAddon.SearchAddon();
@ -126,13 +126,18 @@
}
socket.onmessage = (msg) => {
var re = /:([^\x07]*?)\x07/g;
var re = /:([^\x07].*?)\x07/g;
arr = re.exec(msg.data)
if(arr) {
title = arr[1]+"/";
if (arr[1] === "/") {
title = arr[1];
}
else {
title = arr[1]+"/"
}
}
if(msg==="Closing") {
if(msg === "Closing") {
socket.close();
}
}

Loading…
Cancel
Save