Reshuffled commands, adjusted menus, and added a README

HOL-Theorem-Prover · Nov 23, 2018 · c8f9f8e · c8f9f8e
1 parent aaed819
commit c8f9f8e
Show file tree

Hide file tree

Showing 11 changed files with 194 additions and 41 deletions.
diff --git a/Default (Linux).sublime-keymap b/Default (Linux).sublime-keymap
@@ -102,6 +102,31 @@
 			{ "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
@@ -122,5 +122,30 @@
 			{ "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
@@ -96,5 +96,30 @@
 			{ "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
@@ -0,0 +1,15 @@
+
+[
+    {
+        "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"
+    }
+]
diff --git a/Default.sublime-keymap b/Default.sublime-keymap
diff --git a/SublimeHOL (OSX).sublime-settings → HOL (OSX).sublime-settings b/SublimeHOL (OSX).sublime-settings → HOL (OSX).sublime-settings
diff --git a/Main.sublime-menu b/Main.sublime-menu
@@ -26,7 +26,7 @@
                  "children":
                     [
                         {"caption": "Selection", "command": "hol_repl_transfer_current", "args": {"scope": "selection"}},
-                        {"caption": "Selection (Quiet)", "args": {"scope": "selection", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
+                        {"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"}}
@@ -83,20 +83,53 @@
                         "children":
                         [
                             {
-                                "command": "open_file", "args":
-                                {
-                                    "file": "${packages}/HOL/HOL.sublime-settings"
+                                "command": "open_file",
+                                "args": {
+                                    "file": "${packages}/HOL/Default (OSX).sublime-keymap",
+                                    "platform": "OSX"
                                 },
-                                "caption": "Settings – Default"
+                                "caption": "Key Bindings – Default"
                             },
                             {
-                                "command": "open_file", "args":
-                                {
-                                    "file": "${packages}/User/HOL.sublime-settings"
+                                "command": "open_file",
+                                "args": {
+                                    "file": "${packages}/HOL/Default (Linux).sublime-keymap",
+                                    "platform": "Linux"
                                 },
-                                "caption": "Settings – User"
+                                "caption": "Key Bindings – Default"
                             },
-                            { "caption": "-" }
+                            {
+                                "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": "Key Bindings – User"
+                            },
+                            {
+                                "command": "open_file",
+                                "args": {
+                                    "file": "${packages}/User/Default (Linux).sublime-keymap",
+                                    "platform": "Linux"
+                                },
+                                "caption": "Key Bindings – User"
+                            },
+                            {
+                                "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
@@ -1 +1,59 @@
-HOL - 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.
+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/example_screenshot.png b/example_screenshot.png
diff --git a/packages.json b/packages.json
@@ -3,7 +3,7 @@
     "packages": [{
         "name": "HOL",
         "details": "https://github.com/JamesShaker/SublimeHOL",
-        "description": "A HOL Development Environment with colour REPL.",
+        "description": "A HOL ITP Development Environment with colour REPL.",
         "releases": [
             {
                 "sublime_text": "*",

diff --git 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 = ""