-
Notifications
You must be signed in to change notification settings - Fork 4
/
idriscasesplit.vim
100 lines (89 loc) · 1.99 KB
/
idriscasesplit.vim
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
function IdrisReload()
let file = expand("%")
let tc = system("idris --client :l " . file)
if (! (tc is ""))
echo tc
endif
return tc
endfunction
function IdrisShowType()
w
let word = expand("<cword>")
let tc = IdrisReload()
if (! (tc is ""))
echo tc
else
let ty = system("idris --client :t " . word)
echo ty
endif
return tc
endfunction
function IdrisCaseSplit()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let tc = IdrisReload()
if (tc is "")
let fn = "idris --client :cs! " . cline . " " . word
let result = system(fn)
if (! (result is ""))
echo result
else
e
call winrestview(view)
endif
endif
endfunction
function IdrisMakeWith()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let tc = IdrisReload()
if (tc is "")
let fn = "idris --client :mw! " . cline . " " . word
let result = system(fn)
if (! (result is ""))
echo result
else
e
call winrestview(view)
call search("_")
endif
endif
endfunction
function IdrisAddClause()
let view = winsaveview()
w
let cline = line(".")
let word = expand("<cword>")
let tc = IdrisReload()
if (tc is "")
let fn = "idris --client :ac! " . cline . " " . word
let result = system(fn)
if (! (result is ""))
echo result
else
e
call winrestview(view)
call search(word)
endif
endif
endfunction
function IdrisEval()
let tc = IdrisReload()
if (tc is "")
let expr = input ("Expression: ")
let fn = "idris --client '" . expr . "'"
let result = system(fn)
echo result
endif
echo ""
endfunction
map <LocalLeader>t :call IdrisShowType()<ENTER>
map <LocalLeader>r :call IdrisReload()<ENTER>
map <LocalLeader>c :call IdrisCaseSplit()<ENTER>
map <LocalLeader>d ?:<ENTER>b:call IdrisAddClause()<ENTER>w
map <LocalLeader>w 0:call IdrisMakeWith()<ENTER>
map <LocalLeader>e :call IdrisEval()<ENTER>