diff --git a/tools-poly/configure.sml b/tools-poly/configure.sml index d5af2a2b64..c4eb6d0622 100644 --- a/tools-poly/configure.sml +++ b/tools-poly/configure.sml @@ -517,12 +517,13 @@ val _ = closeOut tar3; output(tar4,"augroup filetypedetect\n"); output(tar4," au BufRead,BufNewFile *.sml let maplocalleader = \"h\" | source "^tar1^"\n"); + output(tar4," au BufRead,BufNewFile *?Script.sml setlocal filetype=hol4script\n"); output(tar4," \" recognise pre-munger files as latex source\n"); output(tar4," au BufRead,BufNewFile *.htex setlocal filetype=htex syntax=tex\n"); output(tar4," \"Uncomment the line below to automatically load Unicode\n"); output(tar4," \"au BufRead,BufNewFile *?Script.sml source "^fullPath [pref, "holabs.vim"]^"\n"); output(tar4," \"Uncomment the line below to fold proofs\n"); - output(tar4," \"au BufRead,BufNewFile *?Script.sml setlocal foldmethod=marker foldmarker=Proof,QED foldnestmax=1\n"); + output(tar4," \"au BufRead,BufNewFile *?Script.sml setlocal foldmethod=syntax foldnestmax=1\n"); output(tar4,"augroup END\n"); closeOut tar4 end; diff --git a/tools/vim/README.md b/tools/vim/README.md index f1b63797f5..23fe341af6 100644 --- a/tools/vim/README.md +++ b/tools/vim/README.md @@ -26,21 +26,24 @@ All files are located under tools/vim - `vimhol.sh`: Wraps hol and vim side-by-side in tmux. Below you find the description of its usage. See below for an alternative approach of running an hol interactive session within vim. +- `hol4script.vim`: Syntax highlighting definitions for HOL4 scripts. - `README.md`: Documentation. (This file.) ## Quickstart 1. Add the contents of `hol-config.sml` to your `~/.hol-config.sml` file 2. Add the contents of `filetype.vim` to your `~/.vim/filetype.vim` -3. Run hol to start the HOL session (only necessary when using vim without +3. Copy `hol4script.vim` to your `~/.vim/syntax/hol4script.vim` +4. Run hol to start the HOL session (only necessary when using vim without support for terminal buffers) -4. Run vim and open a HOL script -5. Select some SML value or declaration and type `hs` to send it to the HOL +5. Run vim and open a HOL script +6. Select some SML value or declaration and type `hs` to send it to the HOL session. See below for more key mappings If you don't have `filetype on` in vim, then this won't work. In that case, you should forget step 2 and source `hol.vim` manually in step 3. To turn filetype -on, you can add `filetype on` to your `~/.vimrc`. +on, you can add `filetype on` to your `~/.vimrc`. Similarly, syntax +highlighting requires `syntax on`. ## WARNING diff --git a/tools/vim/hol4script.vim b/tools/vim/hol4script.vim new file mode 100644 index 0000000000..c71fb1dd29 --- /dev/null +++ b/tools/vim/hol4script.vim @@ -0,0 +1,263 @@ +" Language: HOL4 Script + +""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""" +" +" Custom syntax highlighting for HOL4 script files. Highlights HOL4 terms +" separately from ML syntax, and changes ML syntax highlighting to behave +" slightly differently. +" +""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""" + +syn case match + +syn match MLIdent /\<\(\u\|\l\|_\)\(\w\|'\)*\>/ contained + +syn match MLEscChar /\\\(\l\|\d\d\d\)/ +syn region MLString start=/"/ skip=/\(\\\\\|\\"\)/ end=/"/ contains=MLEscChar +syn match MLCharErr /\(#"\\\d"\|#"\\\d\d"\|#""\|#"[^"\\][^"\\]"\+\)/ +syn match MLChar /#"\\\\"\|#"\(\\\l\|\\\d\d\d\|\\"\|[^"]\)"/ contains=MLEscChar +syn match MLNumber /\~\?\<\d\+\>/ +syn match MLNumber /\~\?\<\d*\.\d\+\([eE][+-]\?\d\+\)\?\>/ + +syn keyword MLTodo TODO XXX NOTE FIXME contained +syn region MLComment start=/(\*/ end=/\*)/ contains=MLComment,MLTodo + +syn keyword MLKeyword let local open in end +syn keyword MLKeyword if then else case of +syn keyword MLKeyword val fun and struct sig +syn keyword MLKeyword infix infixl +syn keyword MLKeyword raise handle +syn keyword MLKeyword structure signature +syn keyword MLKeyword datatype type + +syn keyword MLOperator andalso orelse +syn keyword MLOperator div mod quot +syn keyword MLOperator before rem + +syn match MLOperator ":" +syn match MLOperator ":=" +syn match MLOperator "=>" +syn match MLOperator "::" +syn match MLOperator "\<_\>" +syn match MLOperator "!" +syn match MLOperator ";" +syn match MLOperator "\^" +syn match MLOperator "=" +syn match MLOperator "\*" +syn match MLOperator "+" +syn match MLOperator "-" +syn match MLOperator "/" +syn match MLOperator "|" +syn match MLOperator "\[" +syn match MLOperator "\]" +syn match MLOperator "\]" +syn match MLOperator "\$" + +""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""" +" HOL stuff +""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""" + +syn region HOLString start=/«/ end=/»/ contains=MLEscChar + +" Definition +syn region HOLDefnStart + \ matchgroup=MLKeyword start="^\" + \ end=":"me=e-1 + \ contains=MLIdent nextgroup=HOLDefnEnd +syn match HOLQED /^\/ +syn region HOLDefnEnd + \ matchgroup=MLKeyword start=":" + \ matchgroup=MLKeyword end="^\(\\|\\)" + \ contains=@HOLTerms contained + +" Datatype +syn region HOLDatatype + \ matchgroup=MLKeyword start="^\" + \ end=":"me=e-1 + \ nextgroup=HOLDefnEnd + +" Type, Overload +syn region HOLTypeAbbrev + \ matchgroup=MLKeyword start="^\(\\|\\)" + \ end="="me=e-1 + \ contains=MLIdent,MLString + +" Theorem +syn region HOLThmStart + \ matchgroup=MLKeyword start="^\" + \ end="[:=]"me=e-1 + \ contains=MLIdent,HOLThmExtra + \ nextgroup=HOLThmProof + +syn match HOLThmExtra /\[[^\]]*\]/ms=s+1,me=e-1 contained +syn region HOLThmProof + \ matchgroup=MLKeyword start=":" + \ matchgroup=MLKeyword end="^\"me=e-6 + \ contains=@HOLTerms contained + \ nextgroup=HOLThmProofFold + +syn region HOLThmProofFold + \ matchgroup=MLKeyword start="^\" + \ matchgroup=HOLQED end="^\" + \ transparent fold + +" Triviality +syn region HOLTriviality + \ matchgroup=MLKeyword start="^\" + \ end="[:=]"me=e-1 + \ contains=MLIdent + \ nextgroup=HOLThmProof + +" (Co)Inductive +syn region HOLCoInductive + \ matchgroup=MLKeyword start="^\<\(Co\)\?Inductive\>" + \ end=":"me=e-1 + \ contains=@HOLTerms + \ nextgroup=HOLDefnEnd + +" Tactics and tacticals + +syn match MLTactical "\\\\" +syn match MLTactical ">>" +syn match MLTactical ">-" +syn match MLTactical ">\~" +syn match MLTactical ">>\~" +syn match MLTactical "\" +syn match MLTactical "\" +syn match MLTactical "rpt" +syn match MLCheat "\" +" TODO tactics + +" Single quotes +syn region HOLQuoteSing + \ matchgroup=MLQuote start="\(`\|‘\)" + \ matchgroup=MLQuote end="\(`\|’\)" + \ contains=@HOLTerms +syn region HOLQuoteDoub + \ matchgroup=MLQuote start="\(``\|“\)" + \ matchgroup=MLQuote end="\(``\|”\)" + \ contains=@HOLTerms +syn match HOLQuoteErr /``[^`]*`[^`]/ +" TODO Errors with unicode quotes + +" HOL syntax + +" Any words not in the symbols, nor keywords +syn match HOLIdents /\(\l\|\u\|_\|'\)\+\(\w\|'\)*/ contained + +" Binders +syn region HOLBinder + \ matchgroup=HOLOperator start="\(!\|∀\|∃\|?!\?\|\\\|λ\)" + \ matchgroup=HOLOperator end="\." + \ contains=HOLVars + \ contained +syn match HOLVars /\(\w\|\s\|'\)\+/ contained + +" Operators +syn match HOLOperator "\((\|)\|{\|}\|\[\|\]\)" contained +syn match HOLOperator "\\\\" contained " This is fdomsub +syn match HOLOperator "/\\" contained +syn match HOLOperator "∧" contained +syn match HOLOperator "\\/" contained +syn match HOLOperator "∨" contained +syn match HOLOperator "\~" contained +syn match HOLOperator "¬" contained +syn match HOLOperator "==>" contained +syn match HOLOperator "⇒" contained +syn match HOLOperator "\(<\|>\|=\)" contained +syn match HOLOperator "<=" contained +syn match HOLOperator "≤" contained +syn match HOLOperator ">=" contained +syn match HOLOperator "≥" contained +syn match HOLOperator "<=>" contained +syn match HOLOperator "⇔" contained +syn match HOLOperator "<>" contained +syn match HOLOperator "≠" contained +syn match HOLOperator "\" contained +syn match HOLOperator "∈" contained +syn match HOLOperator "\" contained +syn match HOLOperator "∉" contained +syn match HOLOperator "\(+\|-\|*\|$\)" contained +syn match HOLOperator "\" contained +syn match HOLOperator "∩" contained +syn match HOLOperator "\" contained +syn match HOLOperator "∪" contained +syn match HOLOperator "\" contained +syn match HOLOperator "\" contained +syn match HOLOperator "⊆" contained +syn match HOLOperator "\" contained +syn match HOLOperator "⊂" contained +syn match HOLOperator "\" contained +syn match HOLOperator "++" contained +syn match HOLOperator "+++" contained +syn match HOLOperator "\(=>\||\|:=\|<_\>\)" contained +syn match HOLOperator "\(;\|,\|<|\||>\|::\)" contained +syn match HOLOperator "\<\(T\|F\)\>" contained +syn match HOLOperator "\" contained + +" Various symbols and keywords + +syn keyword HOLSymbol FLAT LIST_REL EVERY MAP FILTER MEM REVERSE LENGTH REPLICATE ALL_DISTINCT contained +syn keyword HOLSymbol FLOOKUP FDIFF fdomsub FEMPTY contained +syn keyword HOLSymbol OPTION_MAP contained +syn keyword HOLSymbol ALOOKUP contained +syn keyword HOLSymbol TAKE DROP contained +syn keyword HOLSymbol IS_SOME IS_NONE SOME NONE ISL ISR INL INR OUTL OUTR contained +syn keyword HOLSymbol INSERT BIGUNION set LIST_TO_SET contained +syn keyword HOLSymbol DIV MOD contained +syn keyword HOLSymbol EL HD TL LUPDATE contained +syn keyword HOLSymbol FST SND contained +syn keyword HOLSymbol divides int_divides contained +syn keyword HOLSymbol with updated_by contained +syn keyword HOLSymbol RTC contained +syn keyword HOLSymbol IS_PREFIX contained +syn keyword HOLSymbol otherwise contained +syn keyword HOLSymbol ARB contained + +" Some monad syntax keywords +syn keyword HOLSymbol fail return mlet lift + +" Keywords +syn keyword HOLKeywords case of let in if then else do od + +" Comments +syn region HOLComment start=/(\*/ end=/\*)/ contains=HOLComment,MLTodo contained + +syn cluster HOLTerms contains=HOLSymbol,HOLOperator,HOLBinder,HOLIdents,HOLKeywords,HOLComment,MLString,HOLString,MLChar,MLCharErr + +""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""" +" Highlighting settings +""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""""" + +syn sync fromstart + +hi link HOLSymbol Type +hi link HOLOperator Underlined +hi link HOLVars NonText +hi link HOLIdents Ignore +hi link HOLKeywords PreProc +hi link HOLComment Comment +hi link HOLString String + +hi link MLTactical Operator +hi link MLCheat Error + +hi link HOLQuoteErr Error +hi link MLQuote Delimiter +hi link HOLThmExtra Special +hi link HOLQED PreProc + +hi link MLKeyword PreProc +hi link MLComment Comment +hi link MLTodo Todo +hi link MLIdent Identifier + +hi link MLOperator Operator +hi link MLChar Character +hi link MLString String +hi link MLNumber Number +hi link MLEscChar SpecialChar +hi link MLCharErr Error + +let b:current_syntax = 'hol4script' +