diff --git a/config/HOL/HOL.sublime-syntax b/config/HOL/HOL.sublime-syntax index df0f878f..5b25beca 100644 --- a/config/HOL/HOL.sublime-syntax +++ b/config/HOL/HOL.sublime-syntax @@ -56,11 +56,11 @@ contexts: scope: constant.language.hol # comparison operators - - match: '<\=|>\=|<|>|\!\=|\=|:=|>>|>-' + - match: '<\=|>\=|<|>|\!\=|\=|:=' scope: keyword.operator.assignment.hol # arithmetic operators - - match: '\*|\+|-|\/|~|\^|div|mod|::|@' + - match: '\*|\+|-|\/|~|\^|div|mod|::|@|>>|>-|THEN|THEN1|THENL|>\||\\' scope: keyword.operator.arithmetic.hol # logical operators diff --git a/repls/sublimehol_repl.py b/repls/sublimehol_repl.py index 03044a34..2fd74a0a 100644 --- a/repls/sublimehol_repl.py +++ b/repls/sublimehol_repl.py @@ -14,12 +14,11 @@ def __init__(self, encoding, cmd=None, **kwds): def write(self, command): #strip the command of terms and strings and comments - stripped_command = re.sub('“([\w\s\S]*?)”','',command) - stripped_command = re.sub('‘([\w\s\S]*?)’','',command) + stripped_command = re.sub('\`\`([\w\s\S]*?)\`\`','',stripped_command) stripped_command = re.sub('\`([\w\s\S]*?)\`','',stripped_command) - stripped_command = re.sub('\"([\w\s\S]*?)\"','',stripped_command) stripped_command = re.sub('\“([\w\s\S]*?)\”','',stripped_command) stripped_command = re.sub('\‘([\w\s\S]*?)\’','',stripped_command) + stripped_command = re.sub('\"([\w\s\S]*?)\"','',stripped_command) stripped_command = re.sub('\(\*([\w\s\S]*?)\*\)','',stripped_command) #get open dependencies @@ -49,5 +48,4 @@ def send_signal(self, sig): if self.is_alive(): #Need to send signal to children because HOL runs everything #in build heap - print("Trying to get group of " + str(self.popen.pid) + " killed with signal " + str(sig)) os.killpg(os.getpgid(self.popen.pid), sig) \ No newline at end of file