diff --git a/Context.sublime-menu b/Context.sublime-menu
index 56002134..8ea5ea5e 100644
--- a/Context.sublime-menu
+++ b/Context.sublime-menu
@@ -1,6 +1,6 @@
 [
 	{"caption": "-"},
-    {"command": "repl_kill", "caption": "Kill"},
-	{"command": "repl_restart", "caption": "Restart"},
-	{"command": "subprocess_repl_send_signal", "caption": "Send other SIGNAL"}
+    {"command": "hol_repl_kill", "caption": "Kill"},
+	{"command": "hol_repl_restart", "caption": "Restart"},
+	{"command": "hol_subprocess_repl_send_signal", "caption": "Send other SIGNAL"}
 ]
\ No newline at end of file
diff --git a/Default (Linux).sublime-keymap b/Default (Linux).sublime-keymap
index 5aaa82ee..b04fdec0 100644
--- a/Default (Linux).sublime-keymap	
+++ b/Default (Linux).sublime-keymap	
@@ -1,5 +1,5 @@
 [
-	{ "keys": ["up"], "command": "repl_view_previous",
+	{ "keys": ["up"], "command": "hol_repl_view_previous",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
@@ -7,14 +7,14 @@
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
 		]
 	},
-	{ "keys": ["alt+p"], "command": "repl_view_previous",
+	{ "keys": ["alt+p"], "command": "hol_repl_view_previous",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["down"], "command": "repl_view_next",
+	{ "keys": ["down"], "command": "hol_repl_view_next",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
@@ -22,35 +22,35 @@
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
 		]
 	},
-	{ "keys": ["alt+n"], "command": "repl_view_next",
+	{ "keys": ["alt+n"], "command": "hol_repl_view_next",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["enter"], "command": "repl_enter", "args": {},
+	{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
 		]
 	},
-	{ "keys": ["enter"], "command": "repl_enter", "args": {},
+	{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
 			{ "key": "setting.auto_complete_commit_on_tab", "operand": true }
 		]
 	},
-	{ "keys": ["escape"], "command": "repl_escape", "args": {},
+	{ "keys": ["escape"], "command": "hol_repl_escape", "args": {},
 	"context":
 		[
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false },
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["backspace"], "command": "repl_backspace", "args": {},
+	{ "keys": ["backspace"], "command": "hol_repl_backspace", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
@@ -58,7 +58,7 @@
 			{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
 		]
 	},
-	{ "keys": ["ctrl+backspace"], "command": "repl_ctrl_backspace", "args": {},
+	{ "keys": ["ctrl+backspace"], "command": "hol_repl_ctrl_backspace", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
@@ -66,42 +66,67 @@
 			{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
 		]
 	},
-	{ "keys": ["left"], "command": "repl_left", "args": {},
+	{ "keys": ["left"], "command": "hol_repl_left", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["home"], "command": "repl_home", "args": {},
+	{ "keys": ["home"], "command": "hol_repl_home", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["shift+left"], "command": "repl_shift_left", "args": {},
+	{ "keys": ["shift+left"], "command": "hol_repl_shift_left", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["shift+home"], "command": "repl_shift_home", "args": {},
+	{ "keys": ["shift+home"], "command": "hol_repl_shift_home", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["ctrl+l"], "command": "repl_clear",
+	{ "keys": ["ctrl+l"], "command": "hol_repl_clear",
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["shift+ctrl+c"], "command": "subprocess_repl_send_signal", "args": {"signal": 2},  // sigint
+	{ "keys": ["shift+ctrl+c"], "command": "hol_subprocess_repl_send_signal", "args": {"signal": 2},  // sigint
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
+	{ "keys": ["ctrl+,", "q", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
+	{ "keys": ["ctrl+,", "q", "l"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
+
+	{ "keys": ["ctrl+,", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection"}},
+	{ "keys": ["ctrl+,", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "g(", "append":");"}},
+	{ "keys": ["ctrl+,", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
+	{ "keys": ["ctrl+,", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
+	{ "keys": ["ctrl+,", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(", "append":");"}},
+
+	{ "keys": ["ctrl+,", "l", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "lines"}},
+	{ "keys": ["ctrl+,", "l", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "g(", "append":");"}},
+	{ "keys": ["ctrl+,", "l", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
+	{ "keys": ["ctrl+,", "l", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
+	{ "keys": ["ctrl+,", "l", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(", "append":");"}},
+
+	{ "keys": ["ctrl+,", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "file"}},
+
+	{ "keys": ["ctrl+,", "p"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "p();"}},
+	{ "keys": ["ctrl+,", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "b();"}},
+	{ "keys": ["ctrl+,", "r"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "restart();"}},
+
+	{ "keys": ["ctrl+,", "f", "y"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_types := (not (!show_types));"}},
+	{ "keys": ["ctrl+,", "f", "a"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_assums := (not (!show_assums));"}},
+	{ "keys": ["ctrl+,", "f", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_at_top\" (1 - current_trace \"Goalstack.print_goal_at_top\");"}},
+	{ "keys": ["ctrl+,", "f", "f"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_fvs\" (1 - current_trace \"Goalstack.print_goal_fvs\");"}}
 
  ]
 
diff --git a/Default (OSX).sublime-keymap b/Default (OSX).sublime-keymap
index 00d1c2e4..6bc794c9 100644
--- a/Default (OSX).sublime-keymap	
+++ b/Default (OSX).sublime-keymap	
@@ -1,5 +1,5 @@
 [
-	{ "keys": ["up"], "command": "repl_view_previous",
+	{ "keys": ["up"], "command": "hol_repl_view_previous",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
@@ -7,14 +7,14 @@
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
 		]
 	},
-	{ "keys": ["ctrl+p"], "command": "repl_view_previous",
+	{ "keys": ["ctrl+p"], "command": "hol_repl_view_previous",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["down"], "command": "repl_view_next",
+	{ "keys": ["down"], "command": "hol_repl_view_next",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
@@ -22,35 +22,35 @@
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
 		]
 	},
-	{ "keys": ["ctrl+n"], "command": "repl_view_next",
+	{ "keys": ["ctrl+n"], "command": "hol_repl_view_next",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["enter"], "command": "repl_enter", "args": {},
+	{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
 		]
 	},
-	{ "keys": ["enter"], "command": "repl_enter", "args": {},
+	{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
 			{ "key": "setting.auto_complete_commit_on_tab", "operand": true }
 		]
 	},
-	{ "keys": ["escape"], "command": "repl_escape", "args": {},
+	{ "keys": ["escape"], "command": "hol_repl_escape", "args": {},
 	"context":
 		[
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false },
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["backspace"], "command": "repl_backspace", "args": {},
+	{ "keys": ["backspace"], "command": "hol_repl_backspace", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
@@ -58,7 +58,7 @@
 			{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
 		]
 	},
-	{ "keys": ["ctrl+backspace"], "command": "repl_ctrl_backspace", "args": {},
+	{ "keys": ["ctrl+backspace"], "command": "hol_repl_ctrl_backspace", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
@@ -66,61 +66,86 @@
 			{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
 		]
 	},
-	{ "keys": ["super+backspace"], "command": "repl_super_backspace", "args": {},
+	{ "keys": ["super+backspace"], "command": "hol_repl_super_backspace", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
 			{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
 		]
 	},
-	{ "keys": ["alt+backspace"], "command": "repl_ctrl_backspace", "args": {},
+	{ "keys": ["alt+backspace"], "command": "hol_repl_ctrl_backspace", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
 			{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
 		]
 	},
-	{ "keys": ["left"], "command": "repl_left", "args": {},
+	{ "keys": ["left"], "command": "hol_repl_left", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["home"], "command": "repl_home", "args": {},
+	{ "keys": ["home"], "command": "hol_repl_home", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["ctrl+a"], "command": "repl_home", "args": {},
+	{ "keys": ["ctrl+a"], "command": "hol_repl_home", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["shift+left"], "command": "repl_shift_left", "args": {},
+	{ "keys": ["shift+left"], "command": "hol_repl_shift_left", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["shift+home"], "command": "repl_shift_home", "args": {},
+	{ "keys": ["shift+home"], "command": "hol_repl_shift_home", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["ctrl+l"], "command": "repl_clear",
+	{ "keys": ["ctrl+l"], "command": "hol_repl_clear",
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["shift+ctrl+c"], "command": "subprocess_repl_send_signal", "args": {"signal": 2},  // sigint
+	{ "keys": ["shift+ctrl+c"], "command": "hol_subprocess_repl_send_signal", "args": {"signal": 2},  // sigint
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
+	{ "keys": ["ctrl+,", "q", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
+	{ "keys": ["ctrl+,", "q", "l"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
+
+	{ "keys": ["ctrl+,", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection"}},
+	{ "keys": ["ctrl+,", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "g(", "append":");"}},
+	{ "keys": ["ctrl+,", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
+	{ "keys": ["ctrl+,", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
+	{ "keys": ["ctrl+,", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(", "append":");"}},
+
+	{ "keys": ["ctrl+,", "l", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "lines"}},
+	{ "keys": ["ctrl+,", "l", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "g(", "append":");"}},
+	{ "keys": ["ctrl+,", "l", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
+	{ "keys": ["ctrl+,", "l", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
+	{ "keys": ["ctrl+,", "l", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(", "append":");"}},
+
+	{ "keys": ["ctrl+,", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "file"}},
+
+	{ "keys": ["ctrl+,", "p"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "p();"}},
+	{ "keys": ["ctrl+,", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "b();"}},
+	{ "keys": ["ctrl+,", "r"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "restart();"}},
+
+	{ "keys": ["ctrl+,", "f", "y"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_types := (not (!show_types));"}},
+	{ "keys": ["ctrl+,", "f", "a"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_assums := (not (!show_assums));"}},
+	{ "keys": ["ctrl+,", "f", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_at_top\" (1 - current_trace \"Goalstack.print_goal_at_top\");"}},
+	{ "keys": ["ctrl+,", "f", "f"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_fvs\" (1 - current_trace \"Goalstack.print_goal_fvs\");"}}
 
 ]
diff --git a/Default (Windows).sublime-keymap b/Default (Windows).sublime-keymap
index b3c7fd3b..d1eedd27 100644
--- a/Default (Windows).sublime-keymap	
+++ b/Default (Windows).sublime-keymap	
@@ -1,5 +1,5 @@
 [
-	{ "keys": ["up"], "command": "repl_view_previous",
+	{ "keys": ["up"], "command": "hol_repl_view_previous",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
@@ -7,14 +7,14 @@
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
 		]
 	},
-	{ "keys": ["alt+p"], "command": "repl_view_previous",
+	{ "keys": ["alt+p"], "command": "hol_repl_view_previous",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["down"], "command": "repl_view_next",
+	{ "keys": ["down"], "command": "hol_repl_view_next",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
@@ -22,35 +22,35 @@
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
 		]
 	},
-	{ "keys": ["alt+n"], "command": "repl_view_next",
+	{ "keys": ["alt+n"], "command": "hol_repl_view_next",
 	"context":
 		[
 			{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["enter"], "command": "repl_enter", "args": {},
+	{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
 		]
 	},
-	{ "keys": ["enter"], "command": "repl_enter", "args": {},
+	{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
 			{ "key": "setting.auto_complete_commit_on_tab", "operand": true }
 		]
 	},
-	{ "keys": ["escape"], "command": "repl_escape", "args": {},
+	{ "keys": ["escape"], "command": "hol_repl_escape", "args": {},
 	"context":
 		[
 			{ "key": "auto_complete_visible", "operator": "equal", "operand": false },
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["backspace"], "command": "repl_backspace", "args": {},
+	{ "keys": ["backspace"], "command": "hol_repl_backspace", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
@@ -58,7 +58,7 @@
 			{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
 		]
 	},
-	{ "keys": ["ctrl+backspace"], "command": "repl_ctrl_backspace", "args": {},
+	{ "keys": ["ctrl+backspace"], "command": "hol_repl_ctrl_backspace", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true },
@@ -66,35 +66,60 @@
 			{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
 		]
 	},
-	{ "keys": ["left"], "command": "repl_left", "args": {},
+	{ "keys": ["left"], "command": "hol_repl_left", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["home"], "command": "repl_home", "args": {},
+	{ "keys": ["home"], "command": "hol_repl_home", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["shift+left"], "command": "repl_shift_left", "args": {},
+	{ "keys": ["shift+left"], "command": "hol_repl_shift_left", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["shift+home"], "command": "repl_shift_home", "args": {},
+	{ "keys": ["shift+home"], "command": "hol_repl_shift_home", "args": {},
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
-	{ "keys": ["shift+ctrl+c"], "command": "repl_clear",
+	{ "keys": ["shift+ctrl+c"], "command": "hol_repl_clear",
 	"context":
 		[
 			{ "key": "setting.repl", "operator": "equal", "operand": true }
 		]
 	},
+	{ "keys": ["ctrl+,", "q", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
+	{ "keys": ["ctrl+,", "q", "l"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
+
+	{ "keys": ["ctrl+,", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection"}},
+	{ "keys": ["ctrl+,", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "g(", "append":");"}},
+	{ "keys": ["ctrl+,", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
+	{ "keys": ["ctrl+,", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
+	{ "keys": ["ctrl+,", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(", "append":");"}},
+
+	{ "keys": ["ctrl+,", "l", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "lines"}},
+	{ "keys": ["ctrl+,", "l", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "g(", "append":");"}},
+	{ "keys": ["ctrl+,", "l", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
+	{ "keys": ["ctrl+,", "l", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
+	{ "keys": ["ctrl+,", "l", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(", "append":");"}},
+
+	{ "keys": ["ctrl+,", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "file"}},
+
+	{ "keys": ["ctrl+,", "p"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "p();"}},
+	{ "keys": ["ctrl+,", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "b();"}},
+	{ "keys": ["ctrl+,", "r"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "restart();"}},
+
+	{ "keys": ["ctrl+,", "f", "y"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_types := (not (!show_types));"}},
+	{ "keys": ["ctrl+,", "f", "a"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_assums := (not (!show_assums));"}},
+	{ "keys": ["ctrl+,", "f", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_at_top\" (1 - current_trace \"Goalstack.print_goal_at_top\");"}},
+	{ "keys": ["ctrl+,", "f", "f"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_fvs\" (1 - current_trace \"Goalstack.print_goal_fvs\");"}}
 
 ]
diff --git a/Default.sublime-commands b/Default.sublime-commands
index 2b3bcfbf..783746e1 100644
--- a/Default.sublime-commands
+++ b/Default.sublime-commands
@@ -1,6 +1,15 @@
+
 [
     {
-        "caption": "SublimeHOL: Restart REPL",
-        "command": "repl_restart"
+        "caption": "HOL: Run REPL",
+        "command": "run_existing_window_command", "args":
+        {
+            "id": "repl_hol",
+            "file": "Main.sublime-menu"
+        }
+    },
+    {
+        "caption": "HOL: Restart REPL",
+        "command": "hol_repl_restart"
     }
-]
+]
\ No newline at end of file
diff --git a/SublimeHOL (OSX).sublime-settings b/HOL (OSX).sublime-settings
similarity index 100%
rename from SublimeHOL (OSX).sublime-settings
rename to HOL (OSX).sublime-settings
diff --git a/SublimeHOL.sublime-settings b/HOL.sublime-settings
similarity index 54%
rename from SublimeHOL.sublime-settings
rename to HOL.sublime-settings
index a1889912..b1e1cbf3 100644
--- a/SublimeHOL.sublime-settings
+++ b/HOL.sublime-settings
@@ -75,51 +75,43 @@
 	//ANSI SETTINGS - Defaults licensed under MIT (see MIT-LICENSE.TXT)
 
 	"ANSI_FG": [
-      {"scope": "black", "code": "\\x1b\\[(0{,2};)?30m", "color": "#000000"},
-      {"scope": "black_light", "code": "\\x1b\\[1;30m", "color": "#686868"},
-      {"scope": "black_bright", "code": "\\x1b\\[90m", "color": "#686868"},
-      {"scope": "red", "code": "\\x1b\\[(0{,2};)?31m", "color": "#c71e12"},
-      {"scope": "red_light", "code": "\\x1b\\[1;31m", "color": "#ff6f6b"},
-      {"scope": "red_bright", "code": "\\x1b\\[91m", "color": "#ff6f6b"},
-      {"scope": "green", "code": "\\x1b\\[(0{,2};)?32m", "color": "#00c120"},
-      {"scope": "green_light", "code": "\\x1b\\[1;32m", "color": "#67f86f"},
-      {"scope": "green_bright", "code": "\\x1b\\[92m", "color": "#67f86f"},
-      {"scope": "yellow", "code": "\\x1b\\[(0{,2};)?33m", "color": "#c7c327"},
-      {"scope": "yellow_light", "code": "\\x1b\\[1;33m", "color": "#fffa72"},
-      {"scope": "yellow_bright", "code": "\\x1b\\[93m", "color": "#fffa72"},
-      {"scope": "blue", "code": "\\x1b\\[(0{,2};)?34m", "color": "#0a2fc4"},
-      {"scope": "blue_light", "code": "\\x1b\\[1;34m", "color": "#6a76fc"},
-      {"scope": "blue_bright", "code": "\\x1b\\[94m", "color": "#6a76fc"},
-      {"scope": "magenta", "code": "\\x1b\\[(0{,2};)?35m", "color": "#c839c5"},
-      {"scope": "magenta_light", "code": "\\x1b\\[1;35m", "color": "#ff7cfd"},
-      {"scope": "magenta_bright", "code": "\\x1b\\[95m", "color": "#ff7cfd"},
-      {"scope": "cyan", "code": "\\x1b\\[(0{,2};)?36m", "color": "#01c5c6"},
-      {"scope": "cyan_light", "code": "\\x1b\\[1;36m", "color": "#68fdfe"},
-      {"scope": "cyan_bright", "code": "\\x1b\\[96m", "color": "#68fdfe"},
-      {"scope": "white", "code": "\\x1b\\[(0{,2};)?(37)?m", "color": "#c7c7c7"},
-      {"scope": "white_light", "code": "\\x1b\\[1;37m", "color": "#ffffff"},
-      {"scope": "white_bright", "code": "\\x1b\\[97m", "color": "#ffffff"},
-      {"scope": "_bold", "code": "\\x1b\\[(0{,2};)?1m", "color": "#ffffff", "font_style": "bold"}
+      {"scope": "black", "code": "\\x1b\\[(\\d{,2};)*?30[m;]", "color": "#000000"},
+      {"scope": "black_bright", "code": "\\x1b\\[(\\d{,2};)*?90[m;]", "color": "#686868"},
+      {"scope": "red", "code": "\\x1b\\[(\\d{,2};)*?31[m;]", "color": "#c71e12"},
+      {"scope": "red_bright", "code": "\\x1b\\[(\\d{,2};)*?91[m;]", "color": "#ff6f6b"},
+      {"scope": "green", "code": "\\x1b\\[(\\d{,2};)*?32[m;]", "color": "#00c120"},
+      {"scope": "green_bright", "code": "\\x1b\\[(\\d{,2};)*?92[m;]", "color": "#67f86f"},
+      {"scope": "yellow", "code": "\\x1b\\[(\\d{,2};)*?33[m;]", "color": "#c7c327"},
+      {"scope": "yellow_bright", "code": "\\x1b\\[(\\d{,2};)*?93[m;]", "color": "#fffa72"},
+      {"scope": "blue", "code": "\\x1b\\[(\\d{,2};)*?34[m;]", "color": "#0a2fc4"},
+      {"scope": "blue_bright", "code": "\\x1b\\[(\\d{,2};)*?94[m;]", "color": "#6a76fc"},
+      {"scope": "magenta", "code": "\\x1b\\[(\\d{,2};)*?35[m;]", "color": "#c839c5"},
+      {"scope": "magenta_bright", "code": "\\x1b\\[(\\d{,2};)*?95[m;]", "color": "#ff7cfd"},
+      {"scope": "cyan", "code": "\\x1b\\[(\\d{,2};)*?36[m;]", "color": "#01c5c6"},
+      {"scope": "cyan_bright", "code": "\\x1b\\[(\\d{,2};)*?96[m;]", "color": "#68fdfe"},
+      {"scope": "white", "code": "\\x1b\\[(\\d{,2};)*?(37)?[m;]", "color": "#c7c7c7"},
+      {"scope": "white_bright", "code": "\\x1b\\[(\\d{,2};)*?97[m;]", "color": "#ffffff"},
+      {"scope": "_bold", "code": "\\x1b\\[(\\d{,2};)*?1[m;]", "color": "#ffffff", "font_style": "bold"}
   ],
   "ANSI_BG": [
       {"scope": "", "code": "(?<!\\x1b\\[0;4[01234567]m)(?<!\\x1b\\[4[01234567]m)", "color": "#010000"},
-      {"scope": "_bg_black", "code": "\\x1b\\[(0{,2};)?40m", "color": "#222222"},
-      {"scope": "_bg_black_bright", "code": "\\x1b\\[(0{,2};)?100m", "color": "#686868"},
-      {"scope": "_bg_red", "code": "\\x1b\\[(0{,2};)?41m", "color": "#c71e12"},
-      {"scope": "_bg_red_bright", "code": "\\x1b\\[(0{,2};)?101m", "color": "#ff6f6b"},
-      {"scope": "_bg_green", "code": "\\x1b\\[(0{,2};)?42m", "color": "#00c120"},
-      {"scope": "_bg_green_bright", "code": "\\x1b\\[(0{,2};)?102m", "color": "#67f86f"},
-      {"scope": "_bg_yellow", "code": "\\x1b\\[(0{,2};)?43m", "color": "#c7c327"},
-      {"scope": "_bg_yellow_bright", "code": "\\x1b\\[(0{,2};)?103m", "color": "#fffa72"},
-      {"scope": "_bg_blue", "code": "\\x1b\\[(0{,2};)?44m", "color": "#0a2fc4"},
-      {"scope": "_bg_blue_bright", "code": "\\x1b\\[(0{,2};)?104m", "color": "#6a76fc"},
-      {"scope": "_bg_magenta", "code": "\\x1b\\[(0{,2};)?45m", "color": "#c839c5"},
-      {"scope": "_bg_magenta_bright", "code": "\\x1b\\[(0{,2};)?105m", "color": "#ff7cfd"},
-      {"scope": "_bg_cyan", "code": "\\x1b\\[(0{,2};)?46m", "color": "#01c5c6"},
-      {"scope": "_bg_cyan_bright", "code": "\\x1b\\[(0{,2};)?106m", "color": "#68fdfe"},
-      {"scope": "_bg_white", "code": "\\x1b\\[(0{,2};)?47m", "color": "#c7c7c7"},
-      {"scope": "_bg_white_bright", "code": "\\x1b\\[(0{,2};)?107m", "color": "#ffffff"},
-      {"scope": "_bold", "code": "\\x1b\\[(0{,2};)?1m", "color": "#010000", "font_style": "bold"}
+      {"scope": "_bg_black", "code": "\\x1b\\[(\\d{,2};)*?40[m;]", "color": "#222222"},
+      {"scope": "_bg_black_bright", "code": "\\x1b\\[(\\d{,2};)*?100[m;]", "color": "#686868"},
+      {"scope": "_bg_red", "code": "\\x1b\\[(\\d{,2};)*?41[m;]", "color": "#c71e12"},
+      {"scope": "_bg_red_bright", "code": "\\x1b\\[(\\d{,2};)*?101[m;]", "color": "#ff6f6b"},
+      {"scope": "_bg_green", "code": "\\x1b\\[(\\d{,2};)*?42[m;]", "color": "#00c120"},
+      {"scope": "_bg_green_bright", "code": "\\x1b\\[(\\d{,2};)*?102[m;]", "color": "#67f86f"},
+      {"scope": "_bg_yellow", "code": "\\x1b\\[(\\d{,2};)*?43[m;]", "color": "#c7c327"},
+      {"scope": "_bg_yellow_bright", "code": "\\x1b\\[(\\d{,2};)*?103[m;]", "color": "#fffa72"},
+      {"scope": "_bg_blue", "code": "\\x1b\\[(\\d{,2};)*?44[m;]", "color": "#0a2fc4"},
+      {"scope": "_bg_blue_bright", "code": "\\x1b\\[(\\d{,2};)*?104[m;]", "color": "#6a76fc"},
+      {"scope": "_bg_magenta", "code": "\\x1b\\[(\\d{,2};)*?45[m;]", "color": "#c839c5"},
+      {"scope": "_bg_magenta_bright", "code": "\\x1b\\[(\\d{,2};)*?105[m;]", "color": "#ff7cfd"},
+      {"scope": "_bg_cyan", "code": "\\x1b\\[(\\d{,2};)*?46[m;]", "color": "#01c5c6"},
+      {"scope": "_bg_cyan_bright", "code": "\\x1b\\[(\\d{,2};)*?106[m;]", "color": "#68fdfe"},
+      {"scope": "_bg_white", "code": "\\x1b\\[(\\d{,2};)*?47[m;]", "color": "#c7c7c7"},
+      {"scope": "_bg_white_bright", "code": "\\x1b\\[(\\d{,2};)*?107[m;]", "color": "#ffffff"},
+      {"scope": "_bold", "code": "\\x1b\\[(\\d{,2};)*?1[m;]", "color": "#010000", "font_style": "bold"}
   ],
   "GENERAL":  {
     "background":       "#000000",
diff --git a/LICENSE.TXT b/LICENSE.TXT
index 4f414acf..b2a621cc 100644
--- a/LICENSE.TXT
+++ b/LICENSE.TXT
@@ -1,3 +1,3 @@
 Everything in this package is licensed under GNU GENERAL PUBLIC LICENSE Version 2
-except for 'ansi.py' which is under THE MIT LICENSE and parts of 'SublimeHOL.sublime-settings'
+except for 'ansi.py' which is under THE MIT LICENSE and parts of 'HOL.sublime-settings'
 as indicated within the file.
diff --git a/Main.sublime-menu b/Main.sublime-menu
index c33b2471..fe799b53 100644
--- a/Main.sublime-menu
+++ b/Main.sublime-menu
@@ -3,55 +3,64 @@
         "id": "tools",
         "children":
         [{
-            "caption": "SublimeHOL",
+            "caption": "HOL",
             "mnemonic": "H",
-            "id": "SublimeHOL",
+            "id": "HOL",
             "children":
             [
-                {"command": "hol_start", 
+                {"command": "hol_repl_open", 
                  "caption": "Open REPL",
+                 "id": "repl_hol",
                  "mnemonic": "O",
+                 "args": {
+                    "type": "hol_repl",
+                    "encoding": "utf8",
+                    "cmd": ["hol"],
+                    "cwd": "$file_path",
+                    "external_id": "hol",
+                    "syntax": "Packages/HOL/config/HOL/HOL.sublime-syntax"
+                    }
                 },
                 { "caption": "-" },
                 {"caption": "Eval in REPL",
                  "children":
                     [
-                        {"caption": "Selection", "command": "repl_transfer_current", "args": {"scope": "selection"}},
-                        {"caption": "Selection (Quiet)", "args": {"scope": "selection", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
-                        {"caption": "Lines", "command": "repl_transfer_current", "args": {"scope": "lines"}},
-                        {"caption": "Lines (Quiet)", "command": "repl_transfer_current", "args": {"scope": "lines", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
-                        {"caption": "File", "command": "repl_transfer_current", "args": {"scope": "file"}}
+                        {"caption": "Selection", "command": "hol_repl_transfer_current", "args": {"scope": "selection"}},
+                        {"caption": "Selection (Quiet)", "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
+                        {"caption": "Lines", "command": "hol_repl_transfer_current", "args": {"scope": "lines"}},
+                        {"caption": "Lines (Quiet)", "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
+                        {"caption": "File", "command": "hol_repl_transfer_current", "args": {"scope": "file"}}
                 ]},
                 {"caption": "Custom Selection Eval in REPL",
                  "children":
                     [
-                        { "caption":"Goal", "command": "repl_transfer_current", "args": {"scope": "selection", "prepend": "g(", "append":");"}},
-                        { "caption":"Subgoal", "command": "repl_transfer_current", "args": {"scope": "selection", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
-                        { "caption":"Sufficient Condition", "command": "repl_transfer_current", "args": {"scope": "selection", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
-                        { "caption":"Tactic", "command": "repl_transfer_current", "args": {"scope": "selection", "prepend": "e(", "append":");"}}
+                        { "caption":"Goal", "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "g(", "append":");"}},
+                        { "caption":"Subgoal", "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
+                        { "caption":"Sufficient Condition", "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
+                        { "caption":"Tactic", "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(", "append":");"}}
                 ]},
                 {"caption": "Custom Line Eval in REPL",
                  "children":
                     [
-                        { "caption":"Goal", "command": "repl_transfer_current", "args": {"scope": "lines", "prepend": "g(", "append":");"}},
-                        { "caption":"Subgoal", "command": "repl_transfer_current", "args": {"scope": "lines", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
-                        { "caption":"Sufficient Condition", "command": "repl_transfer_current", "args": {"scope": "lines", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
-                        { "caption":"Tactic", "command": "repl_transfer_current", "args": {"scope": "lines", "prepend": "e(", "append":");"}}
+                        { "caption":"Goal", "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "g(", "append":");"}},
+                        { "caption":"Subgoal", "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
+                        { "caption":"Sufficient Condition", "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
+                        { "caption":"Tactic", "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(", "append":");"}}
                 ]},
                 {"caption": "REPL Control",
                  "children":
                     [
-                        { "caption":"Print Current Goal", "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "p();"}},
-                        { "caption":"Go Back", "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "b();"}},
-                        { "caption":"Restart Proof", "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "restart();"}},
+                        { "caption":"Print Current Goal", "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "p();"}},
+                        { "caption":"Go Back", "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "b();"}},
+                        { "caption":"Restart Proof", "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "restart();"}},
                 ]},        
                 {"caption": "Toggle Flags On/Off",
                  "children":
                     [
-                        { "caption":"Show Types", "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "show_types := (not (!show_types));"}},
-                        { "caption":"Show Assums", "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "show_assums := (not (!show_assums));"}},
-                        { "caption":"Print Goal at Top", "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_at_top\" (1 - current_trace \"Goalstack.print_goal_at_top\");"}},
-                        { "caption":"Print Free Variables", "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_fvs\" (1 - current_trace \"Goalstack.print_goal_fvs\");"}}
+                        { "caption":"Show Types", "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_types := (not (!show_types));"}},
+                        { "caption":"Show Assums", "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_assums := (not (!show_assums));"}},
+                        { "caption":"Print Goal at Top", "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_at_top\" (1 - current_trace \"Goalstack.print_goal_at_top\");"}},
+                        { "caption":"Print Free Variables", "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_fvs\" (1 - current_trace \"Goalstack.print_goal_fvs\");"}}
                 ]}, 
 
             ]   
@@ -70,24 +79,57 @@
                 "children":
                 [
                     {
-                        "caption": "SublimeHOL",
+                        "caption": "HOL",
                         "children":
                         [
                             {
-                                "command": "open_file", "args":
-                                {
-                                    "file": "${packages}/SublimeHOL/SublimeHOL.sublime-settings"
+                                "command": "open_file",
+                                "args": {
+                                    "file": "${packages}/HOL/Default (OSX).sublime-keymap",
+                                    "platform": "OSX"
+                                },
+                                "caption": "Key Bindings – Default"
+                            },
+                            {
+                                "command": "open_file",
+                                "args": {
+                                    "file": "${packages}/HOL/Default (Linux).sublime-keymap",
+                                    "platform": "Linux"
+                                },
+                                "caption": "Key Bindings – Default"
+                            },
+                            {
+                                "command": "open_file",
+                                "args": {
+                                    "file": "${packages}/HOL/Default (Windows).sublime-keymap",
+                                    "platform": "Windows"
+                                },
+                                "caption": "Key Bindings – Default"
+                            },
+                            {
+                                "command": "open_file",
+                                "args": {
+                                    "file": "${packages}/User/Default (OSX).sublime-keymap",
+                                    "platform": "OSX"
                                 },
-                                "caption": "Settings – Default"
+                                "caption": "Key Bindings – User"
                             },
                             {
-                                "command": "open_file", "args":
-                                {
-                                    "file": "${packages}/User/SublimeHOL.sublime-settings"
+                                "command": "open_file",
+                                "args": {
+                                    "file": "${packages}/User/Default (Linux).sublime-keymap",
+                                    "platform": "Linux"
                                 },
-                                "caption": "Settings – User"
+                                "caption": "Key Bindings – User"
                             },
-                            { "caption": "-" }
+                            {
+                                "command": "open_file",
+                                "args": {
+                                    "file": "${packages}/User/Default (Windows).sublime-keymap",
+                                    "platform": "Windows"
+                                },
+                                "caption": "Key Bindings – User"
+                            }
                         ]
                     }
                 ]
diff --git a/README.md b/README.md
index ab9e44ec..dc932799 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,59 @@
-SublimeHOL - A HOL Development Environment built on top of slimmed down, heavily modified versions of SublimeREPL (https://github.com/wuub/SublimeREPL), SublimeANSI (https://github.com/aziz/SublimeANSI), and SML-syntax (https://github.com/Takaia/SML-syntax) hackily put together.
\ No newline at end of file
+HOL for Sublime Text
+=====================================
+
+A HOL ITP (https://hol-theorem-prover.org/) development environment built on top of slimmed down, heavily modified versions of SublimeREPL (https://github.com/wuub/SublimeREPL), SublimeANSI (https://github.com/aziz/SublimeANSI), and SML-syntax (https://github.com/Takaia/SML-syntax) put together.
+
+![HOL Plugin Screenshot](example_screenshot.png)
+
+Features
+--------
+#### HOL Files
+* HOL Syntax Highlighting
+* Tab completion from `` \` `` to smart quote pair ``‘’``
+    * Also from `` \`\` `` to ``“”``
+* Unicode tab completion within HOL terms for common HOL ASCII sequences
+    * Logical Symbols
+        * ``!`` to ``∀``
+        * ``?`` to ``∃``
+        * ``~`` to ``¬``
+        * ``==>`` to ``⇒``
+        * ...and many more!
+    * The lower case greek alphabet
+        * ``'a`` to ``α``
+        * ``'b`` to ``β``
+        * ... and so on...
+#### HOL REPL
+* Unicode tab completion features in REPL entry also
+* Full colour REPL (Uses HOL's ``vt100_terminal`` backend)
+* Complete REPL history and scrollback
+* Send selection, lines, and entire files straight to REPL in Sublime
+* Automatically format selection/lines into:
+    * Goals
+    * Subgoals
+        * Basic subgoals
+        * Sufficient Condition
+    * Tactics
+    * Quiet mode
+* Changes Flags from menus or key bindings
+    * Show Types
+    * Show Assums
+    * Print Goal at Top
+    * Print Free Variables
+
+Installation
+-------------
+* You must have HOL installed and accessible through the command ``hol``
+* Install the ``HOL`` package from PackageControl (https://packagecontrol.io/)
+* OR clone this repository into your Packages folder and **rename it to HOL**
+
+Usage
+-------
+* ``HOL`` submenu under Tools in Sublime for all the operations and their keybindings
+* A right click context menu exists to kill/restart the REPL and send signals including SIGINT
+* For more details and more control please see the key bindings and preference files available under the preferences menu
+* Note: The terminal is speedy enough for interactive use but large imports should be done in quiet mode as they
+can take some time to colourise!
+
+License
+--------
+Parts of this project are under GPLv2 and parts under MIT, please see LICENSE.txt
diff --git a/ansi.py b/ansi.py
index 695d515c..c7d32f10 100644
--- a/ansi.py
+++ b/ansi.py
@@ -78,7 +78,7 @@ def fast_view_find_all(view, regex_string):
 
 def ansi_definitions(content=None):
 
-    settings = sublime.load_settings("SublimeHOL.sublime-settings")
+    settings = sublime.load_settings("HOL.sublime-settings")
 
     if content is None:
         bgs = settings.get('ANSI_BG', [])
@@ -138,22 +138,22 @@ def subtract_region(p, begin, end):
             return p - (end - begin)
 
 
-class AnsiCommand(sublime_plugin.TextCommand):
+class HolAnsiCommand(sublime_plugin.TextCommand):
 
     def run(self, edit, regions=None, clear_before=False):
         view = self.view
-        if view.settings().get("ansi_in_progress", False):
+        if view.settings().get("hol_ansi_in_progress", False):
             debug(view, "oops ... the ansi command is already in progress")
             return
-        view.settings().set("ansi_in_progress", True)
+        view.settings().set("hol_ansi_in_progress", True)
 
-        view.settings().set("ansi_enabled", True)
-        view.settings().set("color_scheme", "Packages/SublimeHOL/ANSI/ansi.tmTheme")
+        view.settings().set("hol_ansi_enabled", True)
+        view.settings().set("color_scheme", "Packages/User/HOL/ansi.tmTheme")
         view.settings().set("draw_white_space", "none")
 
         # save the view's original scratch and read only settings
-        if not view.settings().has("ansi_scratch"):
-            view.settings().set("ansi_scratch", view.is_scratch())
+        if not view.settings().has("hol_ansi_scratch"):
+            view.settings().set("hol_ansi_scratch", view.is_scratch())
         view.set_scratch(True)
 
         if clear_before:
@@ -164,8 +164,8 @@ def run(self, edit, regions=None, clear_before=False):
         else:
             self._colorize_regions(regions)
 
-        view.settings().set("ansi_in_progress", False)
-        view.settings().set("ansi_size", view.size())
+        view.settings().set("hol_ansi_in_progress", False)
+        view.settings().set("hol_ansi_size", view.size())
 
     def _colorize_regions(self, regions):
         view = self.view
@@ -223,7 +223,7 @@ def _remove_ansi_regions(self):
         for ansi in ansi_definitions():
             view.erase_regions(ansi.scope)
 
-class AnsiColorBuildCommand(Default.exec.ExecCommand):
+class HolAnsiColourBuildCommand(Default.exec.ExecCommand):
 
     process_trigger = "on_finish"
 
@@ -237,7 +237,7 @@ def update_build_settings(self, settings):
             self.process_trigger = val
         else:
             self.process_trigger = None
-            sublime.error_message("SublimeHOL - ANSI settings warning:\n\nThe setting ANSI_process_trigger has been set to an invalid value; must be one of 'on_finish' or 'on_data'.")
+            sublime.error_message("HOL - ANSI settings warning:\n\nThe setting ANSI_process_trigger has been set to an invalid value; must be one of 'on_finish' or 'on_data'.")
 
     @classmethod
     def clear_build_settings(self, settings):
@@ -254,7 +254,7 @@ def auto_string_codec(self, string, encodeOrDecode, encoding='UTF-8'):
     def on_data_process(self, proc, data):
         view = self.output_view
         if not view.settings().get("repl",False):
-            super(AnsiColorBuildCommand, self).on_data(proc, data)
+            super(HolAnsiColourBuildCommand, self).on_data(proc, data)
             return
 
         str_data = self.auto_string_codec(data, 'decode', self.encoding)
@@ -287,7 +287,7 @@ def on_data_process(self, proc, data):
         out_data = self.auto_string_codec(out_data, 'encode', self.encoding)
 
         # send on_data without ansi codes
-        super(AnsiColorBuildCommand, self).on_data(proc, out_data)
+        super(HolAnsiColourBuildCommand, self).on_data(proc, out_data)
 
         # create json serialable region representation
         json_ansi_regions = {}
@@ -297,20 +297,20 @@ def on_data_process(self, proc, data):
             json_ansi_regions.update(region.jsonable())
 
         # send ansi command
-        view.run_command('ansi', args={"regions": json_ansi_regions})
+        view.run_command('hol_ansi', args={"regions": json_ansi_regions})
 
     def on_data(self, proc, data):
         if self.process_trigger == "on_data":
             self.on_data_process(proc, data)
         else:
-            super(AnsiColorBuildCommand, self).on_data(proc, data)
+            super(HolAnsiColourBuildCommand, self).on_data(proc, data)
 
     def on_finished(self, proc):
-        super(AnsiColorBuildCommand, self).on_finished(proc)
+        super(HolAnsiColourBuildCommand, self).on_finished(proc)
         if self.process_trigger == "on_finish":
             view = self.output_view
             if view.settings().get("repl",False):
-                view.run_command("ansi", args={"clear_before": True})
+                view.run_command("hol_ansi", args={"clear_before": True})
 
 
 CS_TEMPLATE = """<?xml version="1.0" encoding="UTF-8"?>
@@ -333,7 +333,7 @@ def on_finished(self, proc):
 
 
 def generate_color_scheme(cs_file, settings):
-    print("Regenerating ANSI color scheme...")
+    print("HOL: Regenerating ANSI color scheme...")
     cs_scopes = ""
     for bg in settings.get("ANSI_BG", []):
         for fg in settings.get("ANSI_FG", []):
@@ -351,9 +351,9 @@ def generate_color_scheme(cs_file, settings):
 
 def plugin_loaded():
     # load pluggin settings
-    settings = sublime.load_settings("SublimeHOL.sublime-settings")
+    settings = sublime.load_settings("HOL.sublime-settings")
     # create ansi color scheme directory
-    ansi_cs_dir = os.path.join(sublime.packages_path(), "SublimeHOL", "ANSI")
+    ansi_cs_dir = os.path.join(sublime.packages_path(), "User", "HOL")
     if not os.path.exists(ansi_cs_dir):
         os.makedirs(ansi_cs_dir)
     # create ansi color scheme file
@@ -361,14 +361,14 @@ def plugin_loaded():
     if not os.path.isfile(cs_file):
         generate_color_scheme(cs_file, settings)
     # update the settings for the plugin
-    AnsiColorBuildCommand.update_build_settings(settings)
-    settings.add_on_change("ANSI_COLORS_CHANGE", lambda: generate_color_scheme(cs_file, settings))
-    settings.add_on_change("ANSI_TRIGGER_CHANGE", lambda: AnsiColorBuildCommand.update_build_settings(settings))
+    HolAnsiColourBuildCommand.update_build_settings(settings)
+    settings.add_on_change("HOL_ANSI_COLORS_CHANGE", lambda: generate_color_scheme(cs_file, settings))
+    settings.add_on_change("HOL_ANSI_TRIGGER_CHANGE", lambda: HolAnsiColourBuildCommand.update_build_settings(settings))
 
 
 def plugin_unloaded():
     # update the settings for the plugin
-    settings = sublime.load_settings("SublimeHOL.sublime-settings")
-    AnsiColorBuildCommand.clear_build_settings(settings)
-    settings.clear_on_change("ANSI_COLORS_CHANGE")
-    settings.clear_on_change("ANSI_TRIGGER_CHANGE")
+    settings = sublime.load_settings("HOL.sublime-settings")
+    HolAnsiColourBuildCommand.clear_build_settings(settings)
+    settings.clear_on_change("HOL_ANSI_COLORS_CHANGE")
+    settings.clear_on_change("HOL_ANSI_TRIGGER_CHANGE")
diff --git a/config/HOL/Default.sublime-commands b/config/HOL/Default.sublime-commands
deleted file mode 100644
index 54ef8fa1..00000000
--- a/config/HOL/Default.sublime-commands
+++ /dev/null
@@ -1,10 +0,0 @@
-[
-    {
-        "caption": "SublimeHOL: HOL",
-        "command": "run_existing_window_command", "args":
-        {
-            "id": "repl_hol",
-            "file": "config/HOL/Main.sublime-menu"
-        }
-    }
-]
\ No newline at end of file
diff --git a/config/HOL/Default.sublime-keymap b/config/HOL/Default.sublime-keymap
deleted file mode 100644
index ffb188c8..00000000
--- a/config/HOL/Default.sublime-keymap
+++ /dev/null
@@ -1,28 +0,0 @@
-[
-{ "keys": ["ctrl+,", "q", "h"], "command": "repl_transfer_current", "args": {"scope": "selection", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
-{ "keys": ["ctrl+,", "q", "l"], "command": "repl_transfer_current", "args": {"scope": "lines", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
-
-{ "keys": ["ctrl+,", "h"], "command": "repl_transfer_current", "args": {"scope": "selection"}},
-{ "keys": ["ctrl+,", "g"], "command": "repl_transfer_current", "args": {"scope": "selection", "prepend": "g(", "append":");"}},
-{ "keys": ["ctrl+,", "s", "g"], "command": "repl_transfer_current", "args": {"scope": "selection", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
-{ "keys": ["ctrl+,", "s", "b"], "command": "repl_transfer_current", "args": {"scope": "selection", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
-{ "keys": ["ctrl+,", "e"], "command": "repl_transfer_current", "args": {"scope": "selection", "prepend": "e(", "append":");"}},
-
-{ "keys": ["ctrl+,", "l", "h"], "command": "repl_transfer_current", "args": {"scope": "lines"}},
-{ "keys": ["ctrl+,", "l", "g"], "command": "repl_transfer_current", "args": {"scope": "lines", "prepend": "g(", "append":");"}},
-{ "keys": ["ctrl+,", "l", "s", "g"], "command": "repl_transfer_current", "args": {"scope": "lines", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
-{ "keys": ["ctrl+,", "l", "s", "b"], "command": "repl_transfer_current", "args": {"scope": "lines", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
-{ "keys": ["ctrl+,", "l", "e"], "command": "repl_transfer_current", "args": {"scope": "lines", "prepend": "e(", "append":");"}},
-
-{ "keys": ["ctrl+,", "t"], "command": "repl_transfer_current", "args": {"scope": "file"}},
-
-{ "keys": ["ctrl+,", "p"], "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "p();"}},
-{ "keys": ["ctrl+,", "b"], "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "b();"}},
-{ "keys": ["ctrl+,", "r"], "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "restart();"}},
-
-{ "keys": ["ctrl+,", "f", "y"], "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "show_types := (not (!show_types));"}},
-{ "keys": ["ctrl+,", "f", "a"], "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "show_assums := (not (!show_assums));"}},
-{ "keys": ["ctrl+,", "f", "t"], "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_at_top\" (1 - current_trace \"Goalstack.print_goal_at_top\");"}},
-{ "keys": ["ctrl+,", "f", "f"], "command": "repl_transfer_current", "args": {"scope": "empty", "prepend": "set_trace \"Goalstack.print_goal_fvs\" (1 - current_trace \"Goalstack.print_goal_fvs\");"}}
-
-]
\ No newline at end of file
diff --git a/config/HOL/Main.sublime-menu b/config/HOL/Main.sublime-menu
deleted file mode 100644
index cc96676e..00000000
--- a/config/HOL/Main.sublime-menu
+++ /dev/null
@@ -1,27 +0,0 @@
-[
-     {
-        "id": "tools",
-        "children":
-        [{
-            "caption": "SublimeHOL",
-            "mnemonic": "H",
-            "id": "SublimeHOL",
-            "children":
-            [
-                {"command": "repl_open", 
-                 "caption": "Open REPL",
-                 "id": "repl_hol",
-                 "mnemonic": "O",
-                 "args": {
-                    "type": "sublime_hol",
-                    "encoding": "utf8",
-                    "cmd": ["hol"],
-                    "cwd": "$file_path",
-                    "external_id": "hol",
-                    "syntax": "Packages/SublimeHOL/config/HOL/HOL.sublime-syntax"
-                    }
-                }
-            ]   
-        }]
-    }
-]
diff --git a/config/Main.sublime-menu.template b/config/Main.sublime-menu.template
deleted file mode 100644
index 9af012d1..00000000
--- a/config/Main.sublime-menu.template
+++ /dev/null
@@ -1,29 +0,0 @@
-[
-     {
-        "id": "tools",
-        "children":
-        [{
-            "caption": "SublimeHOL",
-            "mnemonic": "H",
-            "id": "SublimeHOL",
-            "children":
-            [
-                // {"command": "repl_open",
-                //  "caption": "Command Caption in Menu",
-                //  "mnemonic": "m",
-                //  "args": {
-                //     "type": "subprocess",
-                //     "encoding": "utf8",
-                //     "cmd": ["bash", "-i"] or "bash -i" on windows,
-                //     "cwd": "$file_path",
-                //     "env": {}, // clean environment for subprocess repl
-                //     "extend_env": {}, // variables to be added to standard env
-                //     "cmd_postfix": "\n", // postfix that will be automatically added after a line in repl
-                //     "suppress_echo": false, // try to remove remote echo
-                //     "syntax": "Packages/Text/Plain text.tmLanguage"
-                //     }
-                // },
-            ]
-        }]
-    }
-]
diff --git a/example_screenshot.png b/example_screenshot.png
new file mode 100644
index 00000000..da810aa7
Binary files /dev/null and b/example_screenshot.png differ
diff --git a/packages.json b/packages.json
index 74ca84de..49eb2353 100644
--- a/packages.json
+++ b/packages.json
@@ -1,9 +1,9 @@
 {
     "schema_version": "0.0.1",
     "packages": [{
-        "name": "SublimeHOL",
+        "name": "HOL",
         "details": "https://github.com/JamesShaker/SublimeHOL",
-        "description": "SublimeHOL - A HOL Development Environment built on top of slimmed down, heavily modified versions of SublimeREPL (https://github.com/wuub/SublimeREPL), SublimeANSI (https://github.com/aziz/SublimeANSI), and SML-syntax (https://github.com/Takaia/SML-syntax) hackily put together.",
+        "description": "A HOL ITP Development Environment with colour REPL.",
         "releases": [
             {
                 "sublime_text": "*",
diff --git a/repls/__init__.py b/repls/__init__.py
index 97bbabef..09cfd0e5 100644
--- a/repls/__init__.py
+++ b/repls/__init__.py
@@ -1,3 +1,3 @@
 from .repl import *
 from .subprocess_repl import *
-from .sublimehol_repl import *
\ No newline at end of file
+from .hol_repl import *
\ No newline at end of file
diff --git a/repls/sublimehol_repl.py b/repls/hol_repl.py
similarity index 85%
rename from repls/sublimehol_repl.py
rename to repls/hol_repl.py
index 2fd74a0a..b7c2b6e7 100644
--- a/repls/sublimehol_repl.py
+++ b/repls/hol_repl.py
@@ -5,16 +5,16 @@
 from sublime import load_settings, error_message
 from .subprocess_repl import SubprocessRepl
 
-class SublimeHOLRepl(SubprocessRepl):
-    TYPE = "sublime_hol"
+class HOLRepl(SubprocessRepl):
+    TYPE = "hol_repl"
 
     def __init__(self, encoding, cmd=None, **kwds):
-        super(SublimeHOLRepl, self).__init__(encoding, cmd=cmd, preexec_fn=os.setsid, **kwds)
+        super(HOLRepl, self).__init__(encoding, cmd=cmd, preexec_fn=os.setsid, **kwds)
         self.write("current_backend := PPBackEnd.vt100_terminal;\n")
    
     def write(self, command):
         #strip the command of terms and strings and comments
-        stripped_command = re.sub('\`\`([\w\s\S]*?)\`\`','',stripped_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)
@@ -37,7 +37,7 @@ def write(self, command):
 
         #run final command
         new_cmd = dep_string + command
-        return super(SublimeHOLRepl, self).write(new_cmd)
+        return super(HOLRepl, self).write(new_cmd)
     def send_signal(self, sig):
         if sig == signal.SIGTERM:
             self._killed = True
diff --git a/repls/subprocess_repl.py b/repls/subprocess_repl.py
index c998b2d5..2152d3f3 100644
--- a/repls/subprocess_repl.py
+++ b/repls/subprocess_repl.py
@@ -57,7 +57,7 @@ class SubprocessRepl(Repl):
 
     def __init__(self, encoding, cmd=None, env=None, cwd=None, extend_env=None, soft_quit="", autocomplete_server=False, preexec_fn=None, **kwds):
         super(SubprocessRepl, self).__init__(encoding, **kwds)
-        settings = load_settings('SublimeHOL.sublime-settings')
+        settings = load_settings('HOL.sublime-settings')
 
         if cmd[0] == "[unsupported]":
             raise Unsupported(cmd[1:])
@@ -149,7 +149,7 @@ def getenv(self, settings):
                 import traceback
                 traceback.print_exc()
                 error_message(
-                    "SublimeHOL: obtaining sane environment failed in getenv()\n"
+                    "HOL: obtaining sane environment failed in getenv()\n"
                     "Check console and 'getenv_command' setting \n"
                     "WARN: Falling back to SublimeText environment")
 
diff --git a/run_existing_command.py b/run_existing_command.py
index b2e1ae51..82a7d2f4 100644
--- a/run_existing_command.py
+++ b/run_existing_command.py
@@ -13,17 +13,17 @@
 def plugin_loaded():
     global SUBLIMEHOL_DIR
     global SUBLIMEHOL_USER_DIR
-    SUBLIMEHOL_DIR = "Packages/SublimeHOL"
-    SUBLIMEHOL_USER_DIR = os.path.join(sublime.packages_path(), "User", "SublimeHOL")
+    SUBLIMEHOL_DIR = "Packages/HOL"
+    SUBLIMEHOL_USER_DIR = os.path.join(sublime.packages_path(), "User", "HOL")
 
 PY2 = False
 if sys.version_info[0] == 2:
     SUBLIMEHOL_DIR = os.getcwdu()
-    SUBLIMEHOL_USER_DIR = os.path.join(sublime.packages_path(), "User", "SublimeHOL")
+    SUBLIMEHOL_USER_DIR = os.path.join(sublime.packages_path(), "User", "HOL")
     PY2 = True
 
 # yes, CommandCommmand :) 
-class RunExistingWindowCommandCommand(sublime_plugin.WindowCommand):
+class HolRunExistingWindowCommandCommand(sublime_plugin.WindowCommand):
     def run(self, id, file):
         """Find and run existing command with id in specified file. 
         SUBLIMEHOL_USER_DIR is consulted first, and then SUBLIMEHOL_DIR""" 
diff --git a/sublimehol.py b/sublimehol.py
index de933100..df4a9c4a 100644
--- a/sublimehol.py
+++ b/sublimehol.py
@@ -33,7 +33,7 @@
     PY2 = True
 
 PLATFORM = sublime.platform().lower()
-SETTINGS_FILE = 'SublimeHOL.sublime-settings'
+SETTINGS_FILE = 'HOL.sublime-settings'
 SUBLIME2 = sublime.version() < '3000'
 
 RESTART_MSG = """
@@ -42,19 +42,19 @@
 #############
 """
 
-class ReplInsertTextCommand(sublime_plugin.TextCommand):
+class HolReplInsertTextCommand(sublime_plugin.TextCommand):
     def run(self, edit, pos, text):
         self.view.set_read_only(False)  # make sure view is writable
         self.view.insert(edit, int(pos), text)
 
 
-class ReplEraseTextCommand(sublime_plugin.TextCommand):
+class HolReplEraseTextCommand(sublime_plugin.TextCommand):
     def run(self, edit, start, end):
         self.view.set_read_only(False)  # make sure view is writable
         self.view.erase(edit, sublime.Region(int(start), int(end)))
 
 
-class ReplPass(sublime_plugin.TextCommand):
+class HolReplPass(sublime_plugin.TextCommand):
     def run(self, edit):
         pass
 
@@ -133,7 +133,7 @@ def match(self, command_prefix):
 class PersistentHistory(MemHistory):
     def __init__(self, external_id):
         super(PersistentHistory, self).__init__()
-        path = os.path.join(sublime.packages_path(), "User", ".SublimeHOLHistory")
+        path = os.path.join(sublime.packages_path(), "User", ".HOLHistory")
         if not os.path.isdir(path):
             os.makedirs(path)
         filepath = os.path.join(path, external_id + ".db")
@@ -222,7 +222,7 @@ def __init__(self, view, repl, syntax, repl_restart_args):
             self._window.focus_view(view)
 
         #setup ANSI
-        self._view.run_command('ansi')
+        self._view.run_command('hol_ansi')
         
         # begin refreshing attached view
         self.update_view_loop()
@@ -324,7 +324,7 @@ def adjust_end(self):
             v = self._view
             vsize = v.size()
             self._output_end = min(vsize, self._output_end)
-            v.run_command("repl_erase_text", {"start": self._output_end, "end": vsize})
+            v.run_command("hol_repl_erase_text", {"start": self._output_end, "end": vsize})
         else:
             self._output_end = self._view.size()
 
@@ -379,11 +379,11 @@ def _write_worker(self):
                 out_data = str_data
                 json_ansi_regions = None
             # send on_data without ansi codes
-            self._view.run_command("repl_insert_text", {"pos": self._view.size(), "text": out_data})
+            self._view.run_command("hol_repl_insert_text", {"pos": self._view.size(), "text": out_data})
 
             # send ansi command
             if json_ansi_regions:
-                self._view.run_command('ansi', args={"regions": json_ansi_regions})
+                self._view.run_command('hol_ansi', args={"regions": json_ansi_regions})
             self._output_end += len(out_data)
             self._view.show(self.input_region)
 
@@ -398,7 +398,7 @@ def append_input_text(self, text, edit=None):
         if edit:
             self._view.insert(edit, self._view.size(), text)
         else:
-            self._view.run_command("repl_insert_text", {"pos": self._view.size(), "text": text})
+            self._view.run_command("hol_repl_insert_text", {"pos": self._view.size(), "text": text})
 
     def handle_repl_output(self):
         """Returns new data from Repl and bool indicating if Repl is still
@@ -428,7 +428,7 @@ def handle_repl_packet(self, packet):
                     self._view.add_regions('sublimehol', regions, 'invalid',
                                            '', sublime.DRAW_EMPTY | sublime.DRAW_OUTLINED)
                 else:
-                    print('SublimeHOL: unknown REPL opcode: ' + opcode)
+                    print('HOL: unknown REPL opcode: ' + opcode)
         else:
             self.write(packet)
 
@@ -664,12 +664,12 @@ def _translate_dict(window, dictionary, subst=None):
 
 
 # Opens a new REPL
-class ReplOpenCommand(sublime_plugin.WindowCommand):
+class HolReplOpenCommand(sublime_plugin.WindowCommand):
     def run(self, encoding, type, syntax=None, view_id=None, **kwds):
         manager.open(self.window, encoding, type, syntax, view_id, **kwds)
 
 
-class ReplRestartCommand(sublime_plugin.TextCommand):
+class HolReplRestartCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         manager.restart(self.view, edit)
 
@@ -685,22 +685,22 @@ def is_enabled(self):
 
 
 # Submits the Command to the REPL
-class ReplEnterCommand(sublime_plugin.TextCommand):
+class HolReplEnterCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.enter()
 
 
-class ReplClearCommand(sublime_plugin.TextCommand):
+class HolReplClearCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.clear(edit)
 
 
-# Resets Repl Command Line
-class ReplEscapeCommand(sublime_plugin.TextCommand):
+# Resets HolRepl Command Line
+class HolReplEscapeCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
@@ -717,70 +717,70 @@ def repl_view_delta(sublime_view):
     return rv, delta
 
 
-class ReplBackspaceCommand(sublime_plugin.TextCommand):
+class HolReplBackspaceCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.on_backspace()
 
 
-class ReplCtrlBackspaceCommand(sublime_plugin.TextCommand):
+class HolReplCtrlBackspaceCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.on_ctrl_backspace()
 
 
-class ReplSuperBackspaceCommand(sublime_plugin.TextCommand):
+class HolReplSuperBackspaceCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.on_super_backspace()
 
 
-class ReplLeftCommand(sublime_plugin.TextCommand):
+class HolReplLeftCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.on_left()
 
 
-class ReplShiftLeftCommand(sublime_plugin.TextCommand):
+class HolReplShiftLeftCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.on_shift_left()
 
 
-class ReplHomeCommand(sublime_plugin.TextCommand):
+class HolReplHomeCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.on_home()
 
 
-class ReplShiftHomeCommand(sublime_plugin.TextCommand):
+class HolReplShiftHomeCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.on_shift_home()
 
 
-class ReplViewPreviousCommand(sublime_plugin.TextCommand):
+class HolReplViewPreviousCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.previous_command(edit)
 
 
-class ReplViewNextCommand(sublime_plugin.TextCommand):
+class HolReplViewNextCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
             rv.next_command(edit)
 
 
-class ReplKillCommand(sublime_plugin.TextCommand):
+class HolReplKillCommand(sublime_plugin.TextCommand):
     def run(self, edit):
         rv = manager.repl_view(self.view)
         if rv:
@@ -797,7 +797,7 @@ def is_enabled(self):
 class SublimeHOLListener(sublime_plugin.EventListener):
     def on_selection_modified(self, view):
         rv = manager.repl_view(view)
-        if rv and not view.settings().get("ansi_in_progress", False):
+        if rv and not view.settings().get("hol_ansi_in_progress", False):
             rv.on_selection_modified()
 
     def on_close(self, view):
@@ -813,16 +813,16 @@ def on_text_command(self, view, command_name, args):
         if command_name == 'left_delete':
             # stop backspace on ST3 w/o breaking brackets
             if not rv.allow_deletion():
-                return 'repl_pass', {}
+                return 'hol_repl_pass', {}
 
         if command_name == 'delete_word' and not args.get('forward'):
             # stop ctrl+backspace on ST3 w/o breaking brackets
             if not rv.allow_deletion():
-                return 'repl_pass', {}
+                return 'hol_repl_pass', {}
 
         return None
 
-class SubprocessReplSendSignal(sublime_plugin.TextCommand):
+class HolSubprocessReplSendSignal(sublime_plugin.TextCommand):
     def run(self, edit, signal=None):
         rv = manager.repl_view(self.view)
         subrepl = rv.repl
diff --git a/sublimehol_build_system_hack.py b/sublimehol_build_system_hack.py
index d774c17e..f3d98cb4 100644
--- a/sublimehol_build_system_hack.py
+++ b/sublimehol_build_system_hack.py
@@ -7,7 +7,7 @@
     import Queue as queue
 
 RESULTS = None
-HACK_BUILD_SYSTEM = "Packages/SublimeHOL/sublimehol_build_system_hack.sublime-build"
+HACK_BUILD_SYSTEM = "Packages/HOL/sublimehol_build_system_hack.sublime-build"
 AUTOMATIC_BUILD_SYSTEM = ""
 
 
diff --git a/text_transfer.py b/text_transfer.py
index ebd70f88..f3548de7 100644
--- a/text_transfer.py
+++ b/text_transfer.py
@@ -43,7 +43,7 @@ def wrap(func):
         SENDERS[external_id] = func
     return wrap
 
-class ReplViewWrite(sublime_plugin.TextCommand):
+class HolReplViewWrite(sublime_plugin.TextCommand):
     def run(self, edit, external_id, text):
         for rv in manager.find_repl(external_id):
             rv.append_input_text(text)
@@ -52,7 +52,7 @@ def run(self, edit, external_id, text):
             sublime.error_message("Cannot find REPL for '{0}'".format(external_id))
 
 
-class ReplSend(sublime_plugin.TextCommand):
+class HolReplSend(sublime_plugin.TextCommand):
     def run(self, edit, external_id, text, with_auto_postfix=True):
         for rv in manager.find_repl(external_id):
             if with_auto_postfix:
@@ -66,7 +66,7 @@ def run(self, edit, external_id, text, with_auto_postfix=True):
             sublime.error_message("Cannot find REPL for '{}'".format(external_id))
 
 
-class ReplTransferCurrent(sublime_plugin.TextCommand):
+class HolReplTransferCurrent(sublime_plugin.TextCommand):
     def run(self, edit, scope="selection", action="send", prepend="", append=""):
         text = ""
         if scope == "selection":
@@ -78,7 +78,7 @@ def run(self, edit, scope="selection", action="send", prepend="", append=""):
         elif scope == "file":
             text = self.selected_file()
         text = prepend + text + append
-        cmd = "repl_" + action
+        cmd = "hol_repl_" + action
         self.view.window().run_command(cmd, {"external_id": self.repl_external_id(), "text": text})
 
     def repl_external_id(self):