aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-04-10 16:12:42 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-04-10 19:43:08 +0200
commit7477094b353b48f1bd1f8ee97a8cd69c04be9db9 (patch)
tree4170869fea6012788ad042a53790d2d83bc0fee2
parentcbd7317516eaac4a5f37c896da5ea984ec1bb77a (diff)
CoqIDE: options for syntax highlighting
-rw-r--r--Makefile.build2
-rw-r--r--ide/coq-ssreflect.lang246
-rw-r--r--ide/coq_style.xml12
-rw-r--r--ide/coqide.ml6
-rw-r--r--ide/preferences.ml17
-rw-r--r--ide/preferences.mli1
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