This repository has been archived by the owner on Aug 28, 2020. It is now read-only.
forked from wuub/SublimeREPL
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Default (Linux).sublime-keymap
132 lines (125 loc) · 6.26 KB
/
Default (Linux).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
[
{ "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": ["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": "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": ["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": "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": ["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": ["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":"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\");"}}
]