Skip to content

Commit 057748e

Browse files
mn200mn200
authored
Merge pull request #1 from JamesShaker/master
Incorporate latest work by James
2 parents 4ffb1d7 + c8f9f8e commit 057748e

24 files changed

+384
-302
lines changed

‎Context.sublime-menu‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[
22
{"caption": "-"},
3-
{"command": "repl_kill", "caption": "Kill"},
4-
{"command": "repl_restart", "caption": "Restart"},
5-
{"command": "subprocess_repl_send_signal", "caption": "Send other SIGNAL"}
3+
{"command": "hol_repl_kill", "caption": "Kill"},
4+
{"command": "hol_repl_restart", "caption": "Restart"},
5+
{"command": "hol_subprocess_repl_send_signal", "caption": "Send other SIGNAL"}
66
]

‎Default (Linux).sublime-keymap‎

Lines changed: 40 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,107 +1,132 @@
11
[
2-
{ "keys": ["up"], "command": "repl_view_previous",
2+
{ "keys": ["up"], "command": "hol_repl_view_previous",
33
"context":
44
[
55
{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
66
{ "key": "setting.repl", "operator": "equal", "operand": true },
77
{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
88
]
99
},
10-
{ "keys": ["alt+p"], "command": "repl_view_previous",
10+
{ "keys": ["alt+p"], "command": "hol_repl_view_previous",
1111
"context":
1212
[
1313
{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
1414
{ "key": "setting.repl", "operator": "equal", "operand": true }
1515
]
1616
},
17-
{ "keys": ["down"], "command": "repl_view_next",
17+
{ "keys": ["down"], "command": "hol_repl_view_next",
1818
"context":
1919
[
2020
{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
2121
{ "key": "setting.repl", "operator": "equal", "operand": true },
2222
{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
2323
]
2424
},
25-
{ "keys": ["alt+n"], "command": "repl_view_next",
25+
{ "keys": ["alt+n"], "command": "hol_repl_view_next",
2626
"context":
2727
[
2828
{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
2929
{ "key": "setting.repl", "operator": "equal", "operand": true }
3030
]
3131
},
32-
{ "keys": ["enter"], "command": "repl_enter", "args": {},
32+
{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
3333
"context":
3434
[
3535
{ "key": "setting.repl", "operator": "equal", "operand": true },
3636
{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
3737
]
3838
},
39-
{ "keys": ["enter"], "command": "repl_enter", "args": {},
39+
{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
4040
"context":
4141
[
4242
{ "key": "setting.repl", "operator": "equal", "operand": true },
4343
{ "key": "setting.auto_complete_commit_on_tab", "operand": true }
4444
]
4545
},
46-
{ "keys": ["escape"], "command": "repl_escape", "args": {},
46+
{ "keys": ["escape"], "command": "hol_repl_escape", "args": {},
4747
"context":
4848
[
4949
{ "key": "auto_complete_visible", "operator": "equal", "operand": false },
5050
{ "key": "setting.repl", "operator": "equal", "operand": true }
5151
]
5252
},
53-
{ "keys": ["backspace"], "command": "repl_backspace", "args": {},
53+
{ "keys": ["backspace"], "command": "hol_repl_backspace", "args": {},
5454
"context":
5555
[
5656
{ "key": "setting.repl", "operator": "equal", "operand": true },
5757
{ "key": "setting.repl_sublime2", "operator": "equal", "operand": true },
5858
{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
5959
]
6060
},
61-
{ "keys": ["ctrl+backspace"], "command": "repl_ctrl_backspace", "args": {},
61+
{ "keys": ["ctrl+backspace"], "command": "hol_repl_ctrl_backspace", "args": {},
6262
"context":
6363
[
6464
{ "key": "setting.repl", "operator": "equal", "operand": true },
6565
{ "key": "setting.repl_sublime2", "operator": "equal", "operand": true },
6666
{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
6767
]
6868
},
69-
{ "keys": ["left"], "command": "repl_left", "args": {},
69+
{ "keys": ["left"], "command": "hol_repl_left", "args": {},
7070
"context":
7171
[
7272
{ "key": "setting.repl", "operator": "equal", "operand": true }
7373
]
7474
},
75-
{ "keys": ["home"], "command": "repl_home", "args": {},
75+
{ "keys": ["home"], "command": "hol_repl_home", "args": {},
7676
"context":
7777
[
7878
{ "key": "setting.repl", "operator": "equal", "operand": true }
7979
]
8080
},
81-
{ "keys": ["shift+left"], "command": "repl_shift_left", "args": {},
81+
{ "keys": ["shift+left"], "command": "hol_repl_shift_left", "args": {},
8282
"context":
8383
[
8484
{ "key": "setting.repl", "operator": "equal", "operand": true }
8585
]
8686
},
87-
{ "keys": ["shift+home"], "command": "repl_shift_home", "args": {},
87+
{ "keys": ["shift+home"], "command": "hol_repl_shift_home", "args": {},
8888
"context":
8989
[
9090
{ "key": "setting.repl", "operator": "equal", "operand": true }
9191
]
9292
},
93-
{ "keys": ["ctrl+l"], "command": "repl_clear",
93+
{ "keys": ["ctrl+l"], "command": "hol_repl_clear",
9494
"context":
9595
[
9696
{ "key": "setting.repl", "operator": "equal", "operand": true }
9797
]
9898
},
99-
{ "keys": ["shift+ctrl+c"], "command": "subprocess_repl_send_signal", "args": {"signal": 2}, // sigint
99+
{ "keys": ["shift+ctrl+c"], "command": "hol_subprocess_repl_send_signal", "args": {"signal": 2}, // sigint
100100
"context":
101101
[
102102
{ "key": "setting.repl", "operator": "equal", "operand": true }
103103
]
104104
},
105+
{ "keys": ["ctrl+,", "q", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
106+
{ "keys": ["ctrl+,", "q", "l"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
107+
108+
{ "keys": ["ctrl+,", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection"}},
109+
{ "keys": ["ctrl+,", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "g(", "append":");"}},
110+
{ "keys": ["ctrl+,", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
111+
{ "keys": ["ctrl+,", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
112+
{ "keys": ["ctrl+,", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(", "append":");"}},
113+
114+
{ "keys": ["ctrl+,", "l", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "lines"}},
115+
{ "keys": ["ctrl+,", "l", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "g(", "append":");"}},
116+
{ "keys": ["ctrl+,", "l", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
117+
{ "keys": ["ctrl+,", "l", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
118+
{ "keys": ["ctrl+,", "l", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(", "append":");"}},
119+
120+
{ "keys": ["ctrl+,", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "file"}},
121+
122+
{ "keys": ["ctrl+,", "p"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "p();"}},
123+
{ "keys": ["ctrl+,", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "b();"}},
124+
{ "keys": ["ctrl+,", "r"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "restart();"}},
125+
126+
{ "keys": ["ctrl+,", "f", "y"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_types := (not (!show_types));"}},
127+
{ "keys": ["ctrl+,", "f", "a"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_assums := (not (!show_assums));"}},
128+
{ "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\");"}},
129+
{ "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\");"}}
105130

106131
]
107132

‎Default (OSX).sublime-keymap‎

Lines changed: 43 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,126 +1,151 @@
11
[
2-
{ "keys": ["up"], "command": "repl_view_previous",
2+
{ "keys": ["up"], "command": "hol_repl_view_previous",
33
"context":
44
[
55
{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
66
{ "key": "setting.repl", "operator": "equal", "operand": true },
77
{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
88
]
99
},
10-
{ "keys": ["ctrl+p"], "command": "repl_view_previous",
10+
{ "keys": ["ctrl+p"], "command": "hol_repl_view_previous",
1111
"context":
1212
[
1313
{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
1414
{ "key": "setting.repl", "operator": "equal", "operand": true }
1515
]
1616
},
17-
{ "keys": ["down"], "command": "repl_view_next",
17+
{ "keys": ["down"], "command": "hol_repl_view_next",
1818
"context":
1919
[
2020
{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
2121
{ "key": "setting.repl", "operator": "equal", "operand": true },
2222
{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
2323
]
2424
},
25-
{ "keys": ["ctrl+n"], "command": "repl_view_next",
25+
{ "keys": ["ctrl+n"], "command": "hol_repl_view_next",
2626
"context":
2727
[
2828
{ "key": "setting.history_arrows", "operator": "equal", "operand": false },
2929
{ "key": "setting.repl", "operator": "equal", "operand": true }
3030
]
3131
},
32-
{ "keys": ["enter"], "command": "repl_enter", "args": {},
32+
{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
3333
"context":
3434
[
3535
{ "key": "setting.repl", "operator": "equal", "operand": true },
3636
{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
3737
]
3838
},
39-
{ "keys": ["enter"], "command": "repl_enter", "args": {},
39+
{ "keys": ["enter"], "command": "hol_repl_enter", "args": {},
4040
"context":
4141
[
4242
{ "key": "setting.repl", "operator": "equal", "operand": true },
4343
{ "key": "setting.auto_complete_commit_on_tab", "operand": true }
4444
]
4545
},
46-
{ "keys": ["escape"], "command": "repl_escape", "args": {},
46+
{ "keys": ["escape"], "command": "hol_repl_escape", "args": {},
4747
"context":
4848
[
4949
{ "key": "auto_complete_visible", "operator": "equal", "operand": false },
5050
{ "key": "setting.repl", "operator": "equal", "operand": true }
5151
]
5252
},
53-
{ "keys": ["backspace"], "command": "repl_backspace", "args": {},
53+
{ "keys": ["backspace"], "command": "hol_repl_backspace", "args": {},
5454
"context":
5555
[
5656
{ "key": "setting.repl", "operator": "equal", "operand": true },
5757
{ "key": "setting.repl_sublime2", "operator": "equal", "operand": true },
5858
{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
5959
]
6060
},
61-
{ "keys": ["ctrl+backspace"], "command": "repl_ctrl_backspace", "args": {},
61+
{ "keys": ["ctrl+backspace"], "command": "hol_repl_ctrl_backspace", "args": {},
6262
"context":
6363
[
6464
{ "key": "setting.repl", "operator": "equal", "operand": true },
6565
{ "key": "setting.repl_sublime2", "operator": "equal", "operand": true },
6666
{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
6767
]
6868
},
69-
{ "keys": ["super+backspace"], "command": "repl_super_backspace", "args": {},
69+
{ "keys": ["super+backspace"], "command": "hol_repl_super_backspace", "args": {},
7070
"context":
7171
[
7272
{ "key": "setting.repl", "operator": "equal", "operand": true },
7373
{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
7474
]
7575
},
76-
{ "keys": ["alt+backspace"], "command": "repl_ctrl_backspace", "args": {},
76+
{ "keys": ["alt+backspace"], "command": "hol_repl_ctrl_backspace", "args": {},
7777
"context":
7878
[
7979
{ "key": "setting.repl", "operator": "equal", "operand": true },
8080
{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
8181
]
8282
},
83-
{ "keys": ["left"], "command": "repl_left", "args": {},
83+
{ "keys": ["left"], "command": "hol_repl_left", "args": {},
8484
"context":
8585
[
8686
{ "key": "setting.repl", "operator": "equal", "operand": true }
8787
]
8888
},
89-
{ "keys": ["home"], "command": "repl_home", "args": {},
89+
{ "keys": ["home"], "command": "hol_repl_home", "args": {},
9090
"context":
9191
[
9292
{ "key": "setting.repl", "operator": "equal", "operand": true }
9393
]
9494
},
95-
{ "keys": ["ctrl+a"], "command": "repl_home", "args": {},
95+
{ "keys": ["ctrl+a"], "command": "hol_repl_home", "args": {},
9696
"context":
9797
[
9898
{ "key": "setting.repl", "operator": "equal", "operand": true }
9999
]
100100
},
101-
{ "keys": ["shift+left"], "command": "repl_shift_left", "args": {},
101+
{ "keys": ["shift+left"], "command": "hol_repl_shift_left", "args": {},
102102
"context":
103103
[
104104
{ "key": "setting.repl", "operator": "equal", "operand": true }
105105
]
106106
},
107-
{ "keys": ["shift+home"], "command": "repl_shift_home", "args": {},
107+
{ "keys": ["shift+home"], "command": "hol_repl_shift_home", "args": {},
108108
"context":
109109
[
110110
{ "key": "setting.repl", "operator": "equal", "operand": true }
111111
]
112112
},
113-
{ "keys": ["ctrl+l"], "command": "repl_clear",
113+
{ "keys": ["ctrl+l"], "command": "hol_repl_clear",
114114
"context":
115115
[
116116
{ "key": "setting.repl", "operator": "equal", "operand": true }
117117
]
118118
},
119-
{ "keys": ["shift+ctrl+c"], "command": "subprocess_repl_send_signal", "args": {"signal": 2}, // sigint
119+
{ "keys": ["shift+ctrl+c"], "command": "hol_subprocess_repl_send_signal", "args": {"signal": 2}, // sigint
120120
"context":
121121
[
122122
{ "key": "setting.repl", "operator": "equal", "operand": true }
123123
]
124124
},
125+
{ "keys": ["ctrl+,", "q", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
126+
{ "keys": ["ctrl+,", "q", "l"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend":"HOL_Interactive.toggle_quietdec();\n", "append":"\nHOL_Interactive.toggle_quietdec();"}},
127+
128+
{ "keys": ["ctrl+,", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection"}},
129+
{ "keys": ["ctrl+,", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "g(", "append":");"}},
130+
{ "keys": ["ctrl+,", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
131+
{ "keys": ["ctrl+,", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
132+
{ "keys": ["ctrl+,", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": "e(", "append":");"}},
133+
134+
{ "keys": ["ctrl+,", "l", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "lines"}},
135+
{ "keys": ["ctrl+,", "l", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "g(", "append":");"}},
136+
{ "keys": ["ctrl+,", "l", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
137+
{ "keys": ["ctrl+,", "l", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
138+
{ "keys": ["ctrl+,", "l", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": "e(", "append":");"}},
139+
140+
{ "keys": ["ctrl+,", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "file"}},
141+
142+
{ "keys": ["ctrl+,", "p"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "p();"}},
143+
{ "keys": ["ctrl+,", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "b();"}},
144+
{ "keys": ["ctrl+,", "r"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "restart();"}},
145+
146+
{ "keys": ["ctrl+,", "f", "y"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_types := (not (!show_types));"}},
147+
{ "keys": ["ctrl+,", "f", "a"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": "show_assums := (not (!show_assums));"}},
148+
{ "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\");"}},
149+
{ "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\");"}}
125150

126151
]

0 commit comments

Comments
 (0)