Some Changes

HOL-Theorem-Prover · Nov 23, 2018 · 4ffb1d7 · 4ffb1d7
1 parent a397804
commit 4ffb1d7
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 6 deletions.
diff --git 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
@@ -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)