forked from JamesShaker/SublimeHOL
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Default (OSX).sublime-keymap
153 lines (147 loc) · 7.3 KB
/
Default (OSX).sublime-keymap
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
[
{ "keys": ["up"], "command": "hol_repl_view_previous",
"context":
[
{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
{ "key": "setting.repl", "operator": "equal", "operand": true },
{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
]
},
{ "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": "hol_repl_view_next",
"context":
[
{ "key": "setting.history_arrows", "operator": "equal", "operand": true },
{ "key": "setting.repl", "operator": "equal", "operand": true },
{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
]
},
{ "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": "hol_repl_enter", "args": {},
"context":
[
{ "key": "setting.repl", "operator": "equal", "operand": true },
{ "key": "auto_complete_visible", "operator": "equal", "operand": false }
]
},
{ "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": "hol_repl_escape", "args": {},
"context":
[
{ "key": "auto_complete_visible", "operator": "equal", "operand": false },
{ "key": "setting.repl", "operator": "equal", "operand": true }
]
},
{ "keys": ["backspace"], "command": "hol_repl_backspace", "args": {},
"context":
[
{ "key": "setting.repl", "operator": "equal", "operand": true },
{ "key": "setting.repl_sublime2", "operator": "equal", "operand": true },
{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
]
},
{ "keys": ["ctrl+backspace"], "command": "hol_repl_ctrl_backspace", "args": {},
"context":
[
{ "key": "setting.repl", "operator": "equal", "operand": true },
{ "key": "setting.repl_sublime2", "operator": "equal", "operand": true },
{ "key": "selection_empty", "operator": "equal", "operand": true, "match_all": true }
]
},
{ "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": "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": "hol_repl_left", "args": {},
"context":
[
{ "key": "setting.repl", "operator": "equal", "operand": true }
]
},
{ "keys": ["home"], "command": "hol_repl_home", "args": {},
"context":
[
{ "key": "setting.repl", "operator": "equal", "operand": true }
]
},
{ "keys": ["ctrl+a"], "command": "hol_repl_home", "args": {},
"context":
[
{ "key": "setting.repl", "operator": "equal", "operand": true }
]
},
{ "keys": ["shift+left"], "command": "hol_repl_shift_left", "args": {},
"context":
[
{ "key": "setting.repl", "operator": "equal", "operand": true }
]
},
{ "keys": ["shift+home"], "command": "hol_repl_shift_home", "args": {},
"context":
[
{ "key": "setting.repl", "operator": "equal", "operand": true }
]
},
{ "keys": ["ctrl+l"], "command": "hol_repl_clear",
"context":
[
{ "key": "setting.repl", "operator": "equal", "operand": true }
]
},
{ "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":";\nHOL_Interactive.toggle_quietdec();\n", "append":";\nHOL_Interactive.toggle_quietdec();"}},
{ "keys": ["ctrl+,", "q", "l"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend":";\nHOL_Interactive.toggle_quietdec();\n", "append":";\nHOL_Interactive.toggle_quietdec();"}},
{ "keys": ["ctrl+,", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "append":";"}},
{ "keys": ["ctrl+,", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": ";\ng(", "append":");"}},
{ "keys": ["ctrl+,", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": ";\ne((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
{ "keys": ["ctrl+,", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": ";\ne(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
{ "keys": ["ctrl+,", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "selection", "prepend": ";\ne(", "append":");"}},
{ "keys": ["ctrl+,", "l", "h"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "append":";"}},
{ "keys": ["ctrl+,", "l", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": ";\ng(", "append":");"}},
{ "keys": ["ctrl+,", "l", "s", "g"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": ";\ne((fn q => BasicProvers.byA(q,ALL_TAC)) ", "append":");"}},
{ "keys": ["ctrl+,", "l", "s", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": ";\ne(Tactical.Q_TAC Tactic.SUFF_TAC ", "append":");"}},
{ "keys": ["ctrl+,", "l", "e"], "command": "hol_repl_transfer_current", "args": {"scope": "lines", "prepend": ";\ne(", "append":");"}},
{ "keys": ["ctrl+,", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "file", "prepend":";\n", "append":";"}},
{ "keys": ["ctrl+,", "p"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": ";\np();"}},
{ "keys": ["ctrl+,", "b"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": ";\nb();"}},
{ "keys": ["ctrl+,", "r"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": ";\nrestart();"}},
{ "keys": ["ctrl+,", "d"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": ";\ndrop();"}},
{ "keys": ["ctrl+,", "f", "y"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": ";\nshow_types := (not (!show_types));"}},
{ "keys": ["ctrl+,", "f", "a"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": ";\nshow_assums := (not (!show_assums));"}},
{ "keys": ["ctrl+,", "f", "t"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend": ";\nset_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": ";\nset_trace \"Goalstack.print_goal_fvs\" (1 - current_trace \"Goalstack.print_goal_fvs\");"}},
{ "keys": ["ctrl+,", "f", "q"], "command": "hol_repl_transfer_current", "args": {"scope": "empty", "prepend":";\nHOL_Interactive.toggle_quietdec();"}}
]