xenia/kakoune
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

rc coq: remove unconventional indentation

Browse Source 
The next commit will touch this file.
This commit is contained in:
Johannes Altmanninger 2022-05-08 14:59:26 +02:00
parent fea851b78b
commit 19806a4b4c
1 changed files with 68 additions and 68 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

136
rc/filetype/coq.kak
View File

@ -27,81 +27,81 @@ provide-module coq %{
# Syntax # Syntax
# ------ # ------
# This is a `looks sensible' keyword syntax highlighting, far from being correct. # This is a `looks sensible' keyword syntax highlighting, far from being correct.
# Note that only the core language and the proof language is supported, # Note that only the core language and the proof language is supported,
# the Ltac language is not (for now). # the Ltac language is not (for now).
add-highlighter shared/coq regions add-highlighter shared/coq regions
add-highlighter shared/coq/comment region -recurse \Q(* \Q(* \Q*) fill comment add-highlighter shared/coq/comment region -recurse \Q(* \Q(* \Q*) fill comment
add-highlighter shared/coq/string region (?<!")" (?<!")("")*" fill string add-highlighter shared/coq/string region (?<!")" (?<!")("")*" fill string
add-highlighter shared/coq/command default-region group add-highlighter shared/coq/command default-region group
# This is not any lexical convention of coq, simply highlighting used to make # This is not any lexical convention of coq, simply highlighting used to make
# proofs look better, based on how people usually use notations # proofs look better, based on how people usually use notations
add-highlighter shared/coq/command/ regex [`!@#$%^&*-=+\\:\;|<>/]+ 0:operator add-highlighter shared/coq/command/ regex [`!@#$%^&*-=+\\:\;|<>/]+ 0:operator
add-highlighter shared/coq/command/ regex \(dfs\)|\(bfs\) 0:operator add-highlighter shared/coq/command/ regex \(dfs\)|\(bfs\) 0:operator
add-highlighter shared/coq/command/ regex [()\[\]{}] 0:operator add-highlighter shared/coq/command/ regex [()\[\]{}] 0:operator
# numeral literals # numeral literals
add-highlighter shared/coq/command/ regex [-]?[0-9][0-9_]*(\.[0-9_]+)?([eE][+-][0-9_]+)? 0:value add-highlighter shared/coq/command/ regex [-]?[0-9][0-9_]*(\.[0-9_]+)?([eE][+-][0-9_]+)? 0:value
evaluate-commands %sh{ evaluate-commands %sh{
# These are builtin keywords of the Gallina language (without tactics) # These are builtin keywords of the Gallina language (without tactics)
keywords="_ IF Prop SProp Set Type as at by cofix discriminated else end exists exists2 fix for" keywords="_ IF Prop SProp Set Type as at by cofix discriminated else end exists exists2 fix for"
keywords="${keywords} forall fun if in lazymatch let match multimatch return then using where with" keywords="${keywords} forall fun if in lazymatch let match multimatch return then using where with"
keywords="${keywords} inside outside" keywords="${keywords} inside outside"
# These are (part of) coq top level commands # These are (part of) coq top level commands
commands="Abort About Add Admitted All Arguments Axiom Back BackTo" commands="Abort About Add Admitted All Arguments Axiom Back BackTo"
commands="${commands} Canonical Cd Check Coercion CoFixpoint Collection Compute Conjecture Context Contextual Corollary" commands="${commands} Canonical Cd Check Coercion CoFixpoint Collection Compute Conjecture Context Contextual Corollary"
commands="${commands} Declare Defined Definition Delimit Drop End Eval Example Existential Export" commands="${commands} Declare Defined Definition Delimit Drop End Eval Example Existential Export"
commands="${commands} Fact Fail File Fixpoint Focus From Function Generalizable Global Goal Grab" commands="${commands} Fact Fail File Fixpoint Focus From Function Generalizable Global Goal Grab"
commands="${commands} Hint Hypotheses Hypothesis Immediate Implicit Import Include Inductive" commands="${commands} Hint Hypotheses Hypothesis Immediate Implicit Import Include Inductive"
commands="${commands} Lemma Let Library Load LoadPath Local Locate Module No Notation Opaque" commands="${commands} Lemma Let Library Load LoadPath Local Locate Module No Notation Opaque"
commands="${commands} Parameter Parameters Primitive Print Proof Property Proposition Pwd Qed Quit" commands="${commands} Parameter Parameters Primitive Print Proof Property Proposition Pwd Qed Quit"
commands="${commands} Rec Record Redirect Register Remark Remove Require Reset" commands="${commands} Rec Record Redirect Register Remark Remove Require Reset"
commands="${commands} Section Search SearchAbout SearchHead SearchPattern SearchRewrite Show Strategy" commands="${commands} Section Search SearchAbout SearchHead SearchPattern SearchRewrite Show Strategy"
commands="${commands} Test Theorem Time Timeout Transparent Types Universes Undo Unfocus Unfocused Unset Variable Variables" commands="${commands} Test Theorem Time Timeout Transparent Types Universes Undo Unfocus Unfocused Unset Variable Variables"
# These are (part of) coq's builtin tactics # These are (part of) coq's builtin tactics
tactics="abstract absurd admit all apply assert assert_fails" tactics="abstract absurd admit all apply assert assert_fails"
tactics="${tactics} assert_succeeds assumption auto autoapply" tactics="${tactics} assert_succeeds assumption auto autoapply"
tactics="${tactics} autorewrite autounfold btauto by case cbn" tactics="${tactics} autorewrite autounfold btauto by case cbn"
tactics="${tactics} cbv change clear clearbody cofix compare" tactics="${tactics} cbv change clear clearbody cofix compare"
tactics="${tactics} compute congr congruence constructor contradict" tactics="${tactics} compute congr congruence constructor contradict"
tactics="${tactics} cut cutrewrite cycle decide decompose dependent" tactics="${tactics} cut cutrewrite cycle decide decompose dependent"
tactics="${tactics} destruct discriminate do done double" tactics="${tactics} destruct discriminate do done double"
tactics="${tactics} eapply eassert eauto eexact elim elimtype exact exfalso" tactics="${tactics} eapply eassert eauto eexact elim elimtype exact exfalso"
tactics="${tactics} fail field first firstorder fix fold functional" tactics="${tactics} fail field first firstorder fix fold functional"
tactics="${tactics} generalize guard have hnf idtac induction injection" tactics="${tactics} generalize guard have hnf idtac induction injection"
tactics="${tactics} instantiate intro intros intuition inversion" tactics="${tactics} instantiate intro intros intuition inversion"
tactics="${tactics} inversion_clear lapply lazy last move omega" tactics="${tactics} inversion_clear lapply lazy last move omega"
tactics="${tactics} pattern pose progress red refine reflexivity" tactics="${tactics} pattern pose progress red refine reflexivity"
tactics="${tactics} remember rename repeat replace rewrite right ring" tactics="${tactics} remember rename repeat replace rewrite right ring"
tactics="${tactics} set setoid_reflexivity setoid_replace setoid_rewrite" tactics="${tactics} set setoid_reflexivity setoid_replace setoid_rewrite"
tactics="${tactics} setoid_symmetry setoid_transitivity simpl simple" tactics="${tactics} setoid_symmetry setoid_transitivity simpl simple"
tactics="${tactics} simplify_eq solve specialize split start stop" tactics="${tactics} simplify_eq solve specialize split start stop"
tactics="${tactics} subst symmetry tauto transitivity trivial try" tactics="${tactics} subst symmetry tauto transitivity trivial try"
tactics="${tactics} under unfold unify unlock" tactics="${tactics} under unfold unify unlock"
echo declare-option str-list coq_static_words ${keywords} ${commands} ${tactics} echo declare-option str-list coq_static_words ${keywords} ${commands} ${tactics}
keywords_regex=$(echo ${keywords} | tr ' ' '|') keywords_regex=$(echo ${keywords} | tr ' ' '|')
printf %s " printf %s "
add-highlighter shared/coq/command/ regex \b(${keywords_regex})\b 0:keyword add-highlighter shared/coq/command/ regex \b(${keywords_regex})\b 0:keyword
" "
commands_regex=$(echo ${commands} | tr ' ' '|') commands_regex=$(echo ${commands} | tr ' ' '|')
printf %s " printf %s "
add-highlighter shared/coq/command/ regex ^[\h\n]*(${commands_regex})\b 0:variable add-highlighter shared/coq/command/ regex ^[\h\n]*(${commands_regex})\b 0:variable
" "
tactics_regex=$(echo ${tactics} | tr ' ' '|') tactics_regex=$(echo ${tactics} | tr ' ' '|')
printf %s " printf %s "
add-highlighter shared/coq/command/ regex \b(${tactics_regex})\b 0:keyword add-highlighter shared/coq/command/ regex \b(${tactics_regex})\b 0:keyword
" "
} }
# Indentation # Indentation
# ----------- # -----------
@ -109,10 +109,10 @@ provide-module coq %{
# not based on explicit, unique delimiters, like braces in C-family. # not based on explicit, unique delimiters, like braces in C-family.
# So it is difficult to properly indent using only regex... # So it is difficult to properly indent using only regex...
# Hence here only a simple mechanism of copying indent is done. # Hence here only a simple mechanism of copying indent is done.
define-command -hidden coq-copy-indent-on-newline %{ define-command -hidden coq-copy-indent-on-newline %{
evaluate-commands -draft -itersel %{ evaluate-commands -draft -itersel %{
try %{ execute-keys -draft k <a-x> s ^\h+ <ret> y gh j P } try %{ execute-keys -draft k <a-x> s ^\h+ <ret> y gh j P }
} }
} }
} }