From 7477094b353b48f1bd1f8ee97a8cd69c04be9db9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Apr 2014 16:12:42 +0200
Subject: CoqIDE: options for syntax highlighting
---
Makefile.build | 2 +-
ide/coq-ssreflect.lang | 246 +++++++++++++++++++++++++++++++++++++++++++++++++
ide/coq_style.xml | 12 +++
ide/coqide.ml | 6 ++
ide/preferences.ml | 17 +++-
ide/preferences.mli | 1 +
6 files changed, 282 insertions(+), 2 deletions(-)
create mode 100644 ide/coq-ssreflect.lang
diff --git a/Makefile.build b/Makefile.build
index 2d942d1fb2..91817a94a7 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 0000000000..4c488ae89a
--- /dev/null
+++ b/ide/coq-ssreflect.lang
@@ -0,0 +1,246 @@
+
+
+
+ *.v
+ \(\*
+ \*\)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ \s
+ [_\p{L}]
+ [_\p{L}'\pN]
+ \%{first_ident_char}\%{ident_char}*
+ (\%{ident}*\.)*\%{ident}
+ [-+*{}]
+ \.(\s|\z)
+ (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)
+ (Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)
+ (((Local)|(Global))\%{space}+)?
+ (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)
+ (Qed)|(Defined)|(Admitted)|(Abort)
+ ((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))
+
+
+ ""
+
+
+ "
+ "
+
+
+
+
+
+ do
+ last
+ first
+
+
+ apply
+ auto
+ case
+ case
+ congr
+ elim
+ exists
+ have
+ gen have
+ generally have
+ move
+ pose
+ rewrite
+ set
+ split
+ suffices
+ suff
+ transitivity
+ without loss
+ wlog
+
+
+ by
+ exact
+ reflexivity
+
+
+
+
+
+ \(\*\*(\s|\z)
+ \*\)
+
+
+
+
+
+
+
+
+ \%{decl_head}
+ \%{dot_sep}
+
+
+
+
+
+
+ forall
+ fun
+ match
+ fix
+ cofix
+ with
+ for
+ end
+ as
+ let
+ in
+ if
+ then
+ else
+ return
+ using
+
+
+ Prop
+ Set
+ Type
+
+
+ \.\.
+
+
+
+
+
+
+
+ Proof
+ \%{end_proof}\%{dot_sep}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ \%{dot_sep}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ \%{undotted_sep}
+
+
+ Add
+ Check
+ Eval
+ Load
+ Undo
+ Goal
+ Print
+ Save
+ Comments
+ Solve\%{space}+Obligation
+ ((Uns)|(S))et(\%{space}+\%{ident})+
+ (\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation
+ \%{locality}Infix
+ (Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist)
+
+
+ \%{locality}Hint\%{space}+
+ Resolve
+ Immediate
+ Constructors
+ unfold
+ Opaque
+ Transparent
+ Extern
+
+
+ \%{space}+Scope
+ \%{locality}Open
+ \%{locality}Close
+ Bind
+ Delimit
+
+
+ \%{space}+(?'qua'\%{qualit})
+ Chapter
+ Combined\%{space}+Scheme
+ End
+ Section
+ Arguments
+ Implicit\%{space}+Arguments
+ (Import)|(Include)
+ Require(\%{space}+((Import)|(Export)))?
+ (Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))?
+ Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive)
+
+
+
+
+
+ (?'qua_list'(\%{space}+\%{qualit})+)
+ Typeclasses (Transparent)|(Opaque)
+
+
+
+
+
+
+
+
diff --git a/ide/coq_style.xml b/ide/coq_style.xml
index 85ea4d891d..67631d3462 100644
--- a/ide/coq_style.xml
+++ b/ide/coq_style.xml
@@ -11,4 +11,16 @@
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 783f4b4316..df0733f7ef 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 585dce21f4..b774ac8427 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 26dc51f399..a93767751d 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
--
cgit v1.2.3