diff options
-rw-r--r-- | Makefile.build | 2 | ||||
-rw-r--r-- | ide/coq-ssreflect.lang | 246 | ||||
-rw-r--r-- | ide/coq_style.xml | 12 | ||||
-rw-r--r-- | ide/coqide.ml | 6 | ||||
-rw-r--r-- | ide/preferences.ml | 17 | ||||
-rw-r--r-- | ide/preferences.mli | 1 |
6 files changed, 282 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index 2d942d1fb..91817a94a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -297,7 +297,7 @@ COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) .SUFFIXES:.vo -IDEFILES=ide/coq.lang ide/coq_style.xml ide/coq.png ide/mac_default_accel_map +IDEFILES=$(wildcard ide/coq*.lang) ide/coq_style.xml ide/coq.png ide/mac_default_accel_map coqide-binaries: coqide-$(HASCOQIDE) coqide-no: diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang new file mode 100644 index 000000000..4c488ae89 --- /dev/null +++ b/ide/coq-ssreflect.lang @@ -0,0 +1,246 @@ +<?xml version="1.0" encoding="UTF-8"?> +<language id="coq-ssreflect" _name="Coq + Ssreflect" version="2.0" _section="Scientific"> + <metadata> + <property name="globs">*.v</property> + <property name="block-comment-start">\(\*</property> + <property name="block-comment-stop">\*\)</property> + </metadata> + + <styles> + <style id="comment" _name="Comment" map-to="def:comment"/> + <style id="coqdoc" _name="Coqdoc text" map-to="def:note"/> + <style id="vernac-keyword" _name="Vernacular keyword" map-to="def:keyword"/> + <style id="gallina-keyword" _name="Gallina keyword" map-to="def:keyword"/> + <style id="identifier" _name="Identifier" map-to="def:identifier"/> + <style id="constr-keyword" _name="Cic keyword" map-to="def:keyword"/> + <style id="constr-sort" _name="Cic sort" map-to="def:builtin"/> + <style id="string" _name="String" map-to="def:string"/> + <style id="escape" _name="Escaped Character" map-to="def:special-char"/> + <style id="error" _name="Error" map-to="def:error"/> + <style id="safe" _name="Checked Part"/> + <style id="sentence" _name="Sentence terminator"/> + <style id="tactic" _name="Tactic"/> + <style id="endtactic" _name="Tactic terminator"/> + <style id="iterator" _name="Tactic iterator"/> + </styles> + + <definitions> + <define-regex id="space">\s</define-regex> + <define-regex id="first_ident_char">[_\p{L}]</define-regex> + <define-regex id="ident_char">[_\p{L}'\pN]</define-regex> + <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex> + <define-regex id="qualit">(\%{ident}*\.)*\%{ident}</define-regex> + <define-regex id="undotted_sep">[-+*{}]</define-regex> + <define-regex id="dot_sep">\.(\s|\z)</define-regex> + <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex> + <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex> + <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex> + <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex> + <define-regex id="end_proof">(Qed)|(Defined)|(Admitted)|(Abort)</define-regex> + <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))</define-regex> + + <context id="escape-seq" style-ref="escape"> + <match>""</match> + </context> + <context id="string" style-ref="string"> + <start>"</start> + <end>"</end> + <include> + <context ref="escape-seq"/> + </include> + </context> + <context id="ssr-iter" style-ref="iterator"> + <keyword>do</keyword> + <keyword>last</keyword> + <keyword>first</keyword> + </context> + <context id="ssr-tac" style-ref="tactic"> + <keyword>apply</keyword> + <keyword>auto</keyword> + <keyword>case</keyword> + <keyword>case</keyword> + <keyword>congr</keyword> + <keyword>elim</keyword> + <keyword>exists</keyword> + <keyword>have</keyword> + <keyword>gen have</keyword> + <keyword>generally have</keyword> + <keyword>move</keyword> + <keyword>pose</keyword> + <keyword>rewrite</keyword> + <keyword>set</keyword> + <keyword>split</keyword> + <keyword>suffices</keyword> + <keyword>suff</keyword> + <keyword>transitivity</keyword> + <keyword>without loss</keyword> + <keyword>wlog</keyword> + </context> + <context id="ssr-endtac" style-ref="endtactic"> + <keyword>by</keyword> + <keyword>exact</keyword> + <keyword>reflexivity</keyword> + </context> + <context id="coq-ssreflect" class="no-spell-check"> + <include> + <context ref="string"/> + <context id="coqdoc" style-ref="coqdoc" class-disabled="no-spell-check"> + <start>\(\*\*(\s|\z)</start> + <end>\*\)</end> + <include> + <context ref="comment-in-comment"/> + <context ref="string"/> + <context ref="escape-seq"/> + </include> + </context> + <context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check"> + <start>\(\*</start> + <end>\*\)</end> + <include> + <context id="comment-in-comment" style-ref="comment" class="comment" class-disabled="no-spell-check"> + <start>\(\*</start> + <end>\*\)</end> + <include> + <context ref="comment-in-comment"/> + <context ref="string"/> + <context ref="escape-seq"/> + </include> + </context> + <context ref="string"/> + <context ref="escape-seq"/> + </include> + </context> + <context id="declaration"> + <start>\%{decl_head}</start> + <end>\%{dot_sep}</end> + <include> + <context sub-pattern="id" where="start" style-ref="identifier"/> + <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/> + <context sub-pattern="id_list" where="start" style-ref="identifier"/> + <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/> + <context id="constr-keyword" style-ref="constr-keyword"> + <keyword>forall</keyword> + <keyword>fun</keyword> + <keyword>match</keyword> + <keyword>fix</keyword> + <keyword>cofix</keyword> + <keyword>with</keyword> + <keyword>for</keyword> + <keyword>end</keyword> + <keyword>as</keyword> + <keyword>let</keyword> + <keyword>in</keyword> + <keyword>if</keyword> + <keyword>then</keyword> + <keyword>else</keyword> + <keyword>return</keyword> + <keyword>using</keyword> + </context> + <context id="constr-sort" style-ref="constr-sort"> + <keyword>Prop</keyword> + <keyword>Set</keyword> + <keyword>Type</keyword> + </context> + <context id="dot-nosep"> + <match>\.\.</match> + </context> + <context ref="comment"/> + <context ref="string"/> + <context ref="coqdoc"/> + </include> + </context> + <context id="proof"> + <start>Proof</start> + <end>\%{end_proof}\%{dot_sep}</end> + <include> + <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> + <context sub-pattern="0" where="end" style-ref="vernac-keyword"/> + <context ref="command"/> + <context ref="scope-command"/> + <context ref="hint-command"/> + <context ref="command-for-qualit"/> + <context ref="declaration"/> + <context ref="comment"/> + <context ref="string"/> + <context ref="coqdoc"/> + <context ref="proof"/> + <context ref="undotted-sep"/> + <context id="tactic" extend-parent="false"> + <start></start> + <end>\%{dot_sep}</end> + <include> + <context ref="ssr-tac"/> + <context ref="ssr-endtac"/> + <context ref="ssr-iter"/> + <context ref="dot-nosep"/> + <context ref="constr-keyword"/> + <context ref="constr-sort"/> + <context ref="comment"/> + <context ref="string"/> + </include> + </context> + </include> + </context> + <context id="undotted-sep" style-ref="vernac-keyword"> + <match>\%{undotted_sep}</match> + </context> + <context id="command" style-ref="vernac-keyword"> + <keyword>Add</keyword> + <keyword>Check</keyword> + <keyword>Eval</keyword> + <keyword>Load</keyword> + <keyword>Undo</keyword> + <keyword>Goal</keyword> + <keyword>Print</keyword> + <keyword>Save</keyword> + <keyword>Comments</keyword> + <keyword>Solve\%{space}+Obligation</keyword> + <keyword>((Uns)|(S))et(\%{space}+\%{ident})+</keyword> + <keyword>(\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation</keyword> + <keyword>\%{locality}Infix</keyword> + <keyword>(Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)</keyword> + </context> + <context id="hint-command" style-ref="vernac-keyword"> + <prefix>\%{locality}Hint\%{space}+</prefix> + <keyword>Resolve</keyword> + <keyword>Immediate</keyword> + <keyword>Constructors</keyword> + <keyword>unfold</keyword> + <keyword>Opaque</keyword> + <keyword>Transparent</keyword> + <keyword>Extern</keyword> + </context> + <context id="scope-command" style-ref="vernac-keyword"> + <suffix>\%{space}+Scope</suffix> + <keyword>\%{locality}Open</keyword> + <keyword>\%{locality}Close</keyword> + <keyword>Bind</keyword> + <keyword>Delimit</keyword> + </context> + <context id="command-for-qualit"> + <suffix>\%{space}+(?'qua'\%{qualit})</suffix> + <keyword>Chapter</keyword> + <keyword>Combined\%{space}+Scheme</keyword> + <keyword>End</keyword> + <keyword>Section</keyword> + <keyword>Arguments</keyword> + <keyword>Implicit\%{space}+Arguments</keyword> + <keyword>(Import)|(Include)</keyword> + <keyword>Require(\%{space}+((Import)|(Export)))?</keyword> + <keyword>(Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?</keyword> + <keyword>Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive)</keyword> + <include> + <context sub-pattern="1" style-ref="vernac-keyword"/> + </include> + </context> + <context id="command-for-qualit-list" style-ref="vernac-keyword"> + <suffix>(?'qua_list'(\%{space}+\%{qualit})+)</suffix> + <keyword>Typeclasses (Transparent)|(Opaque)</keyword> + <include> + <context sub-pattern="qua_list" style-ref="identifier"/> + </include> + </context> + </include> + </context> + </definitions> +</language> diff --git a/ide/coq_style.xml b/ide/coq_style.xml index 85ea4d891..67631d346 100644 --- a/ide/coq_style.xml +++ b/ide/coq_style.xml @@ -11,4 +11,16 @@ <style name="coq:identifier" foreground="#navy"/> <style name="coq:constr-keyword" foreground="#dark green"/> <style name="coq:constr-sort" foreground="#008080"/> + +<style name="coq-ssreflect:comment" foreground="#b22222"/> +<style name="coq-ssreflect:coqdoc" foreground="#b22222" italic="true"/> +<style name="coq-ssreflect:vernac-keyword" bold="true" foreground="#a021f0"/> +<style name="coq-ssreflect:gallina-keyword" bold="true" foreground="#a021f0"/> +<style name="coq-ssreflect:identifier" bold="true" foreground="#0000ff"/> +<style name="coq-ssreflect:constr-keyword" foreground="#228b22"/> +<style name="coq-ssreflect:constr-sort" foreground="#228b22"/> +<style name="coq-ssreflect:tactic" foreground="#101092"/> +<style name="coq-ssreflect:endtactic" foreground="#ff3f3f"/> +<style name="coq-ssreflect:iterator" foreground="#be6ad4"/> +<style name="coq-ssreflect:string" foreground="#8b2252"/> </style-scheme> diff --git a/ide/coqide.ml b/ide/coqide.ml index 783f4b431..df0733f7e 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1267,12 +1267,18 @@ let build_ui () = let iter_session v = v.script#source_buffer#set_style_scheme style in List.iter iter_session notebook#pages in + let refresh_language () = + let lang = lang_manager#language prefs.source_language in + let iter_session v = v.script#source_buffer#set_language lang in + List.iter iter_session notebook#pages + in let resize_window () = w#resize ~width:prefs.window_width ~height:prefs.window_height in refresh_toolbar (); refresh_toolbar_hook := refresh_toolbar; refresh_style_hook := refresh_style; + refresh_language_hook := refresh_language; refresh_editor_hook := refresh_editor_prefs; resize_window_hook := resize_window; refresh_tabs_hook := refresh_notebook_pos; diff --git a/ide/preferences.ml b/ide/preferences.ml index 585dce21f..b774ac842 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -78,6 +78,7 @@ let inputenc_of_string s = (** Hooks *) let refresh_style_hook = ref (fun () -> ()) +let refresh_language_hook = ref (fun () -> ()) let refresh_editor_hook = ref (fun () -> ()) let refresh_toolbar_hook = ref (fun () -> ()) let contextual_menus_on_goal_hook = ref (fun x -> ()) @@ -657,6 +658,19 @@ let configure ?(apply=(fun () -> ())) () = style_manager#style_scheme_ids current.source_style in + let source_language = + let f s = + current.source_language <- s; + !refresh_language_hook () + in + combo "Language:" + ~f ~new_allowed:false + (List.filter + (fun x -> Str.string_match (Str.regexp "^coq") x 0) + lang_manager#language_ids) + current.source_language + in + let read_project = combo "Project file options are" @@ -794,7 +808,8 @@ let configure ?(apply=(fun () -> ())) () = let cmds = [Section("Fonts", Some `SELECT_FONT, [config_font]); - Section("Colors", Some `SELECT_COLOR, [config_color; source_style]); + Section("Colors", Some `SELECT_COLOR, + [config_color; source_language; source_style]); Section("Editor", Some `EDIT, [config_editor]); Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; diff --git a/ide/preferences.mli b/ide/preferences.mli index 26dc51f39..a93767751 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -95,6 +95,7 @@ val configure : ?apply:(unit -> unit) -> unit -> unit (* Hooks *) val refresh_editor_hook : (unit -> unit) ref val refresh_style_hook : (unit -> unit) ref +val refresh_language_hook : (unit -> unit) ref val refresh_toolbar_hook : (unit -> unit) ref val resize_window_hook : (unit -> unit) ref val refresh_tabs_hook : (unit -> unit) ref |