From fed7d0f693128ae2a7c19a519882f12f138d88b4 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Wed, 2 May 2012 17:11:23 +0000
Subject: Coqide highligthing is back (done by gtksourceview).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15269 85f007b7-540e-0410-9357-904b9bb8a0f7
---
Makefile.build | 4 +-
ide/coq.lang | 201 +++++++++++++++++++++++++++++++++++++++++++++++++
ide/coq_style.xml | 14 ++++
ide/preferences.ml | 4 +-
theories/Vectors/Fin.v | 1 +
5 files changed, 220 insertions(+), 4 deletions(-)
create mode 100644 ide/coq.lang
create mode 100644 ide/coq_style.xml
diff --git a/Makefile.build b/Makefile.build
index ef2bb067d3..5b490148db 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -285,7 +285,7 @@ COQIDEFLAGS=-thread $(COQIDEINCLUDES)
.SUFFIXES:.vo
-IDEFILES=ide/coq.png ide/mac_default_accel_map
+IDEFILES=ide/coq.lang ide/coq_style.xml ide/coq.png ide/mac_default_accel_map
coqide-binaries: coqide-$(HASCOQIDE)
coqide-no:
@@ -336,7 +336,7 @@ endif
install-ide-files:
$(MKDIR) $(FULLDATADIR)
- $(INSTALLLIB) ide/coq.png $(FULLDATADIR)
+ $(INSTALLLIB) ide/coq.png ide/coq.lang ide/coq_style.xml $(FULLDATADIR)
$(MKDIR) $(FULLCONFIGDIR)
if [ $(IDEOPTINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi
diff --git a/ide/coq.lang b/ide/coq.lang
new file mode 100644
index 0000000000..daac4c181d
--- /dev/null
+++ b/ide/coq.lang
@@ -0,0 +1,201 @@
+
+
+
+ *.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)|(Include)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)
+ (Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)
+ (((Local)|(Global))\%{space}+)?
+ (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)
+ (Qed)|(Defined)|(Admitted)|(Abort)
+ ((?'gal'(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})+))
+
+
+ \\(\\|"|'|n|t|b|r)
+
+
+ "
+ "
+
+
+
+
+
+
+
+ \(\*\*(\s|\z)
+ \*\)
+
+
+
+
+
+
+
+
+ \%{decl_head}
+ \%{dot_sep}
+
+
+
+
+
+
+ forall
+ fun
+ match
+ fix
+ cofix
+ with
+ for
+ end
+ as
+ let
+ in
+ if
+ then
+ else
+ return
+
+
+ Prop
+ Set
+ Type
+
+
+ \.\.
+
+
+
+
+
+
+ Proof
+ \%{end_proof}\%{dot_sep}
+
+
+
+
+
+
+
+
+
+
+
+
+
+ \b[^-+*{}]
+ \%{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
+ 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
new file mode 100644
index 0000000000..85ea4d891d
--- /dev/null
+++ b/ide/coq_style.xml
@@ -0,0 +1,14 @@
+
+
+The Coq Dev Team
+<_description>Coq/Ssreflect color scheme for the vernacular language
+
+
+
+
+
+
+
+
+
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 8606370b70..3600363d62 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -160,8 +160,8 @@ let (current:pref ref) =
auto_save_delay = 10000;
auto_save_name = "#","#";
- source_language = "vernac";
- source_style = "classic";
+ source_language = "coq";
+ source_style = "coq_style";
read_project = Ignore_args;
project_file_name = "_CoqProject";
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index 717139a0a4..b5736f22d7 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -145,6 +145,7 @@ Qed.
[fin (n + m)]
Really really ineficient !!! *)
Definition L_R {m} n (p : t m) : t (n + m).
+Proof.
induction n.
exact p.
exact ((fix LS k (p: t k) :=
--
cgit v1.2.3