Skip to content

Commit 9e3cd77

Browse files
hrutvikoskarabrahamsson
authored and
mn200
committed
[vim-mode] syntax highlighting and syntax-directed proof folding
Co-authored-by: Oskar Abrahamsson <oskarabrahamsson@users.noreply.github.com>
1 parent efcf2bc commit 9e3cd77

File tree

3 files changed

+272
-5
lines changed

3 files changed

+272
-5
lines changed

‎tools-poly/configure.sml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -517,12 +517,13 @@ val _ =
517517
closeOut tar3;
518518
output(tar4,"augroup filetypedetect\n");
519519
output(tar4," au BufRead,BufNewFile *.sml let maplocalleader = \"h\" | source "^tar1^"\n");
520+
output(tar4," au BufRead,BufNewFile *?Script.sml setlocal filetype=hol4script\n");
520521
output(tar4," \" recognise pre-munger files as latex source\n");
521522
output(tar4," au BufRead,BufNewFile *.htex setlocal filetype=htex syntax=tex\n");
522523
output(tar4," \"Uncomment the line below to automatically load Unicode\n");
523524
output(tar4," \"au BufRead,BufNewFile *?Script.sml source "^fullPath [pref, "holabs.vim"]^"\n");
524525
output(tar4," \"Uncomment the line below to fold proofs\n");
525-
output(tar4," \"au BufRead,BufNewFile *?Script.sml setlocal foldmethod=marker foldmarker=Proof,QED foldnestmax=1\n");
526+
output(tar4," \"au BufRead,BufNewFile *?Script.sml setlocal foldmethod=syntax foldnestmax=1\n");
526527
output(tar4,"augroup END\n");
527528
closeOut tar4
528529
end;

‎tools/vim/README.md

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -26,21 +26,24 @@ All files are located under tools/vim
2626
- `vimhol.sh`: Wraps hol and vim side-by-side in tmux. Below you find the
2727
description of its usage. See below for an alternative approach of running
2828
an hol interactive session within vim.
29+
- `hol4script.vim`: Syntax highlighting definitions for HOL4 scripts.
2930
- `README.md`: Documentation. (This file.)
3031

3132
## Quickstart
3233

3334
1. Add the contents of `hol-config.sml` to your `~/.hol-config.sml` file
3435
2. Add the contents of `filetype.vim` to your `~/.vim/filetype.vim`
35-
3. Run hol to start the HOL session (only necessary when using vim without
36+
3. Copy `hol4script.vim` to your `~/.vim/syntax/hol4script.vim`
37+
4. Run hol to start the HOL session (only necessary when using vim without
3638
support for terminal buffers)
37-
4. Run vim and open a HOL script
38-
5. Select some SML value or declaration and type `hs` to send it to the HOL
39+
5. Run vim and open a HOL script
40+
6. Select some SML value or declaration and type `hs` to send it to the HOL
3941
session. See below for more key mappings
4042

4143
If you don't have `filetype on` in vim, then this won't work. In that case, you
4244
should forget step 2 and source `hol.vim` manually in step 3. To turn filetype
43-
on, you can add `filetype on` to your `~/.vimrc`.
45+
on, you can add `filetype on` to your `~/.vimrc`. Similarly, syntax
46+
highlighting requires `syntax on`.
4447

4548
## WARNING
4649

‎tools/vim/hol4script.vim

Lines changed: 263 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,263 @@
1+
" Language: HOL4 Script
2+
3+
"""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""
4+
"
5+
" Custom syntax highlighting for HOL4 script files. Highlights HOL4 terms
6+
" separately from ML syntax, and changes ML syntax highlighting to behave
7+
" slightly differently.
8+
"
9+
"""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""
10+
11+
syn case match
12+
13+
syn match MLIdent /\<\(\u\|\l\|_\)\(\w\|'\)*\>/ contained
14+
15+
syn match MLEscChar /\\\(\l\|\d\d\d\)/
16+
syn region MLString start=/"/ skip=/\(\\\\\|\\"\)/ end=/"/ contains=MLEscChar
17+
syn match MLCharErr /\(#"\\\d"\|#"\\\d\d"\|#""\|#"[^"\\][^"\\]"\+\)/
18+
syn match MLChar /#"\\\\"\|#"\(\\\l\|\\\d\d\d\|\\"\|[^"]\)"/ contains=MLEscChar
19+
syn match MLNumber /\~\?\<\d\+\>/
20+
syn match MLNumber /\~\?\<\d*\.\d\+\([eE][+-]\?\d\+\)\?\>/
21+
22+
syn keyword MLTodo TODO XXX NOTE FIXME contained
23+
syn region MLComment start=/(\*/ end=/\*)/ contains=MLComment,MLTodo
24+
25+
syn keyword MLKeyword let local open in end
26+
syn keyword MLKeyword if then else case of
27+
syn keyword MLKeyword val fun and struct sig
28+
syn keyword MLKeyword infix infixl
29+
syn keyword MLKeyword raise handle
30+
syn keyword MLKeyword structure signature
31+
syn keyword MLKeyword datatype type
32+
33+
syn keyword MLOperator andalso orelse
34+
syn keyword MLOperator div mod quot
35+
syn keyword MLOperator before rem
36+
37+
syn match MLOperator ":"
38+
syn match MLOperator ":="
39+
syn match MLOperator "=>"
40+
syn match MLOperator "::"
41+
syn match MLOperator "\<_\>"
42+
syn match MLOperator "!"
43+
syn match MLOperator ";"
44+
syn match MLOperator "\^"
45+
syn match MLOperator "="
46+
syn match MLOperator "\*"
47+
syn match MLOperator "+"
48+
syn match MLOperator "-"
49+
syn match MLOperator "/"
50+
syn match MLOperator "|"
51+
syn match MLOperator "\["
52+
syn match MLOperator "\]"
53+
syn match MLOperator "\]"
54+
syn match MLOperator "\$"
55+
56+
"""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""
57+
" HOL stuff
58+
"""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""
59+
60+
syn region HOLString start=/«/ end=/»/ contains=MLEscChar
61+
62+
" Definition
63+
syn region HOLDefnStart
64+
\ matchgroup=MLKeyword start="^\<Definition\>"
65+
\ end=":"me=e-1
66+
\ contains=MLIdent nextgroup=HOLDefnEnd
67+
syn match HOLQED /^\<End\>/
68+
syn region HOLDefnEnd
69+
\ matchgroup=MLKeyword start=":"
70+
\ matchgroup=MLKeyword end="^\(\<End\>\|\<Termination\>\)"
71+
\ contains=@HOLTerms contained
72+
73+
" Datatype
74+
syn region HOLDatatype
75+
\ matchgroup=MLKeyword start="^\<Datatype\>"
76+
\ end=":"me=e-1
77+
\ nextgroup=HOLDefnEnd
78+
79+
" Type, Overload
80+
syn region HOLTypeAbbrev
81+
\ matchgroup=MLKeyword start="^\(\<Type\>\|\<Overload\>\)"
82+
\ end="="me=e-1
83+
\ contains=MLIdent,MLString
84+
85+
" Theorem
86+
syn region HOLThmStart
87+
\ matchgroup=MLKeyword start="^\<Theorem\>"
88+
\ end="[:=]"me=e-1
89+
\ contains=MLIdent,HOLThmExtra
90+
\ nextgroup=HOLThmProof
91+
92+
syn match HOLThmExtra /\[[^\]]*\]/ms=s+1,me=e-1 contained
93+
syn region HOLThmProof
94+
\ matchgroup=MLKeyword start=":"
95+
\ matchgroup=MLKeyword end="^\<Proof\>"me=e-6
96+
\ contains=@HOLTerms contained
97+
\ nextgroup=HOLThmProofFold
98+
99+
syn region HOLThmProofFold
100+
\ matchgroup=MLKeyword start="^\<Proof\>"
101+
\ matchgroup=HOLQED end="^\<QED\>"
102+
\ transparent fold
103+
104+
" Triviality
105+
syn region HOLTriviality
106+
\ matchgroup=MLKeyword start="^\<Triviality\>"
107+
\ end="[:=]"me=e-1
108+
\ contains=MLIdent
109+
\ nextgroup=HOLThmProof
110+
111+
" (Co)Inductive
112+
syn region HOLCoInductive
113+
\ matchgroup=MLKeyword start="^\<\(Co\)\?Inductive\>"
114+
\ end=":"me=e-1
115+
\ contains=@HOLTerms
116+
\ nextgroup=HOLDefnEnd
117+
118+
" Tactics and tacticals
119+
120+
syn match MLTactical "\\\\"
121+
syn match MLTactical ">>"
122+
syn match MLTactical ">-"
123+
syn match MLTactical ">\~"
124+
syn match MLTactical ">>\~"
125+
syn match MLTactical "\<THEN[1L]\?\>"
126+
syn match MLTactical "\<ORELSE\>"
127+
syn match MLTactical "rpt"
128+
syn match MLCheat "\<cheat\>"
129+
" TODO tactics
130+
131+
" Single quotes
132+
syn region HOLQuoteSing
133+
\ matchgroup=MLQuote start="\(`\|‘\)"
134+
\ matchgroup=MLQuote end="\(`\|’\)"
135+
\ contains=@HOLTerms
136+
syn region HOLQuoteDoub
137+
\ matchgroup=MLQuote start="\(``\|“\)"
138+
\ matchgroup=MLQuote end="\(``\|”\)"
139+
\ contains=@HOLTerms
140+
syn match HOLQuoteErr /``[^`]*`[^`]/
141+
" TODO Errors with unicode quotes
142+
143+
" HOL syntax
144+
145+
" Any words not in the symbols, nor keywords
146+
syn match HOLIdents /\(\l\|\u\|_\|'\)\+\(\w\|'\)*/ contained
147+
148+
" Binders
149+
syn region HOLBinder
150+
\ matchgroup=HOLOperator start="\(!\|∀\|∃\|?!\?\|\\\|λ\)"
151+
\ matchgroup=HOLOperator end="\."
152+
\ contains=HOLVars
153+
\ contained
154+
syn match HOLVars /\(\w\|\s\|'\)\+/ contained
155+
156+
" Operators
157+
syn match HOLOperator "\((\|)\|{\|}\|\[\|\]\)" contained
158+
syn match HOLOperator "\\\\" contained " This is fdomsub
159+
syn match HOLOperator "/\\" contained
160+
syn match HOLOperator "∧" contained
161+
syn match HOLOperator "\\/" contained
162+
syn match HOLOperator "∨" contained
163+
syn match HOLOperator "\~" contained
164+
syn match HOLOperator "¬" contained
165+
syn match HOLOperator "==>" contained
166+
syn match HOLOperator "⇒" contained
167+
syn match HOLOperator "\(<\|>\|=\)" contained
168+
syn match HOLOperator "<=" contained
169+
syn match HOLOperator "≤" contained
170+
syn match HOLOperator ">=" contained
171+
syn match HOLOperator "≥" contained
172+
syn match HOLOperator "<=>" contained
173+
syn match HOLOperator "⇔" contained
174+
syn match HOLOperator "<>" contained
175+
syn match HOLOperator "≠" contained
176+
syn match HOLOperator "\<IN\>" contained
177+
syn match HOLOperator "∈" contained
178+
syn match HOLOperator "\<NOTIN\>" contained
179+
syn match HOLOperator "∉" contained
180+
syn match HOLOperator "\(+\|-\|*\|$\)" contained
181+
syn match HOLOperator "\<INTER\>" contained
182+
syn match HOLOperator "∩" contained
183+
syn match HOLOperator "\<UNION\>" contained
184+
syn match HOLOperator "∪" contained
185+
syn match HOLOperator "\<DIFF\>" contained
186+
syn match HOLOperator "\<SUBSET\>" contained
187+
syn match HOLOperator "⊆" contained
188+
syn match HOLOperator "\<PSUBSET\>" contained
189+
syn match HOLOperator "⊂" contained
190+
syn match HOLOperator "\<EMPTY\>" contained
191+
syn match HOLOperator "++" contained
192+
syn match HOLOperator "+++" contained
193+
syn match HOLOperator "\(=>\||\|:=\|<_\>\)" contained
194+
syn match HOLOperator "\(;\|,\|<|\||>\|::\)" contained
195+
syn match HOLOperator "\<\(T\|F\)\>" contained
196+
syn match HOLOperator "\<o\>" contained
197+
198+
" Various symbols and keywords
199+
200+
syn keyword HOLSymbol FLAT LIST_REL EVERY MAP FILTER MEM REVERSE LENGTH REPLICATE ALL_DISTINCT contained
201+
syn keyword HOLSymbol FLOOKUP FDIFF fdomsub FEMPTY contained
202+
syn keyword HOLSymbol OPTION_MAP contained
203+
syn keyword HOLSymbol ALOOKUP contained
204+
syn keyword HOLSymbol TAKE DROP contained
205+
syn keyword HOLSymbol IS_SOME IS_NONE SOME NONE ISL ISR INL INR OUTL OUTR contained
206+
syn keyword HOLSymbol INSERT BIGUNION set LIST_TO_SET contained
207+
syn keyword HOLSymbol DIV MOD contained
208+
syn keyword HOLSymbol EL HD TL LUPDATE contained
209+
syn keyword HOLSymbol FST SND contained
210+
syn keyword HOLSymbol divides int_divides contained
211+
syn keyword HOLSymbol with updated_by contained
212+
syn keyword HOLSymbol RTC contained
213+
syn keyword HOLSymbol IS_PREFIX contained
214+
syn keyword HOLSymbol otherwise contained
215+
syn keyword HOLSymbol ARB contained
216+
217+
" Some monad syntax keywords
218+
syn keyword HOLSymbol fail return mlet lift
219+
220+
" Keywords
221+
syn keyword HOLKeywords case of let in if then else do od
222+
223+
" Comments
224+
syn region HOLComment start=/(\*/ end=/\*)/ contains=HOLComment,MLTodo contained
225+
226+
syn cluster HOLTerms contains=HOLSymbol,HOLOperator,HOLBinder,HOLIdents,HOLKeywords,HOLComment,MLString,HOLString,MLChar,MLCharErr
227+
228+
"""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""
229+
" Highlighting settings
230+
"""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""
231+
232+
syn sync fromstart
233+
234+
hi link HOLSymbol Type
235+
hi link HOLOperator Underlined
236+
hi link HOLVars NonText
237+
hi link HOLIdents Ignore
238+
hi link HOLKeywords PreProc
239+
hi link HOLComment Comment
240+
hi link HOLString String
241+
242+
hi link MLTactical Operator
243+
hi link MLCheat Error
244+
245+
hi link HOLQuoteErr Error
246+
hi link MLQuote Delimiter
247+
hi link HOLThmExtra Special
248+
hi link HOLQED PreProc
249+
250+
hi link MLKeyword PreProc
251+
hi link MLComment Comment
252+
hi link MLTodo Todo
253+
hi link MLIdent Identifier
254+
255+
hi link MLOperator Operator
256+
hi link MLChar Character
257+
hi link MLString String
258+
hi link MLNumber Number
259+
hi link MLEscChar SpecialChar
260+
hi link MLCharErr Error
261+
262+
let b:current_syntax = 'hol4script'
263+

0 commit comments

Comments
 (0)