From 3e28afcde1e1c6423c0d2ef9d88094cbd9c5a68c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 14:45:38 +0100 Subject: Fix syntax highlighting of "Require multiple libraries". --- ide/coq.lang | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 608a4aeaea..6f7994fae7 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -195,7 +195,6 @@ Import Include Export - Require(\%{space}+((Import)|(Export)))? (Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))? Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive) @@ -206,6 +205,7 @@ (?'qua_list'(\%{space}+\%{qualit})+) Typeclasses (Transparent)|(Opaque) + Require(\%{space}+((Import)|(Export)))? -- cgit v1.2.3 From 7dd73ff65ad78b20ff25170f33d15a06ac006ae2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 14:46:04 +0100 Subject: Add syntax highlighting for Coercion. --- ide/coq.lang | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 6f7994fae7..733f1dcec7 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,7 +29,7 @@ (\%{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) + (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)|(Coercion) (Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?) (((Local)|(Global))\%{space}+)? (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property) -- cgit v1.2.3 From d0801d05923278f3dd908c7965085cc052063944 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 14:53:44 +0100 Subject: Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context. --- ide/coq.lang | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 733f1dcec7..94ee77ae1b 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,8 +29,8 @@ (\%{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)|(Coercion) - (Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?) + (Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion) + (Hypothes[ie]s)|(Axiom(s)?)|(Variable(s)?)|(Parameter(s)?)|(Context)|(Implicit\%{space}+Type(s)?) (((Local)|(Global))\%{space}+)? (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property) (Qed)|(Defined)|(Admitted)|(Abort) -- cgit v1.2.3 From c907b5717fd4ef98a5774ab568e2c16d25ce2786 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 14:59:33 +0100 Subject: Fix syntax highlighting of Save. --- ide/coq.lang | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 94ee77ae1b..d634bc1d6c 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -33,7 +33,7 @@ (Hypothes[ie]s)|(Axiom(s)?)|(Variable(s)?)|(Parameter(s)?)|(Context)|(Implicit\%{space}+Type(s)?) (((Local)|(Global))\%{space}+)? (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property) - (Qed)|(Defined)|(Admitted)|(Abort) + (Qed)|(Defined)|(Admitted)|(Abort)|(Save) ((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))|(?'gal2'Goal) @@ -158,7 +158,6 @@ Load Undo Print - Save Comments Solve\%{space}+Obligation ((Uns)|(S))et(\%{space}+\%{ident})+ -- cgit v1.2.3 From f3fdaff32e20c1a05defd2670cffaa3eee752eaf Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 15:03:07 +0100 Subject: Add syntax highlighting for About. --- ide/coq.lang | 1 + 1 file changed, 1 insertion(+) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index d634bc1d6c..46d91816a7 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -189,6 +189,7 @@ Combined\%{space}+Scheme End Section + About Arguments Implicit\%{space}+Arguments Import -- cgit v1.2.3 From 560e06e3409003bb58b158cf5f156eb3db70c227 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 15:08:31 +0100 Subject: Do not highlight "using" as a constr keyword. --- ide/coq.lang | 1 - 1 file changed, 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 46d91816a7..09b59d4625 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -97,7 +97,6 @@ then else return - using Prop -- cgit v1.2.3 From af41885b0e13fff713fef71f9a653e39add9b2f6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 15:22:08 +0100 Subject: Fix syntax highlighting of Scheme. --- ide/coq.lang | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 09b59d4625..788ad8aef8 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,7 +29,7 @@ (\%{ident}\.)*\%{ident} [-+*{}] \.(\s|\z) - (Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion) + (Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion) (Hypothes[ie]s)|(Axiom(s)?)|(Variable(s)?)|(Parameter(s)?)|(Context)|(Implicit\%{space}+Type(s)?) (((Local)|(Global))\%{space}+)? (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property) @@ -186,6 +186,7 @@ \%{space}+(?'qua'\%{qualit}) Chapter Combined\%{space}+Scheme + Scheme\%{space}((Induction)|(Minimality)|(Elimination)|(Case)|(Equality))\%{space}for End Section About -- cgit v1.2.3 From c1587dfec7ecbd48e2404d8c4744eacfce08a943 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 16:03:09 +0100 Subject: Fix syntax highlighting of Require. --- ide/coq.lang | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 788ad8aef8..43268b0c31 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -202,11 +202,12 @@ - + (?'qua_list'(\%{space}+\%{qualit})+) Typeclasses (Transparent)|(Opaque) Require(\%{space}+((Import)|(Export)))? + -- cgit v1.2.3 From 5743fd25fa058e4cf7b5949b8287935163de9232 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 16:03:40 +0100 Subject: Add syntax highlighting for Declare ML Module. --- ide/coq.lang | 1 + 1 file changed, 1 insertion(+) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 43268b0c31..1842f7942a 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -163,6 +163,7 @@ (\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation \%{locality}Infix (Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist) + Declare\%{space}+ML\%{space}+Module \%{locality}Hint\%{space}+ -- cgit v1.2.3 From 1fb3573621dfeb32efea23c26a9164056706f55e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 16:04:30 +0100 Subject: Fix syntax highlighting of Import and Export. --- ide/coq.lang | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 1842f7942a..269bed9381 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -193,9 +193,7 @@ About Arguments Implicit\%{space}+Arguments - Import Include - Export (Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))? Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive) @@ -207,6 +205,8 @@ (?'qua_list'(\%{space}+\%{qualit})+) Typeclasses (Transparent)|(Opaque) Require(\%{space}+((Import)|(Export)))? + Import + Export -- cgit v1.2.3 From 69fb6b654cf02ca0e8b57feef6cf1c31effe6cc4 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 16:06:38 +0100 Subject: Add syntax highlighting for Declare Module. --- ide/coq.lang | 1 + 1 file changed, 1 insertion(+) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 269bed9381..8531702701 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -190,6 +190,7 @@ Scheme\%{space}((Induction)|(Minimality)|(Elimination)|(Case)|(Equality))\%{space}for End Section + Declare\%{space}+Module(\%{space}+((Import)|(Export)))? About Arguments Implicit\%{space}+Arguments -- cgit v1.2.3 From b4abf41dc6a6b2c6471185d6c102dbe1460a32cd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 16:07:13 +0100 Subject: Fix syntax highlighting of Extract Inductive. --- ide/coq.lang | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 8531702701..1622e13330 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -196,7 +196,7 @@ Implicit\%{space}+Arguments Include (Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))? - Extract\%{space}+(Inlined\%{space}+)?(Constant)|(Inductive) + Extract\%{space}+((Inlined\%{space}+)?(Constant)|(Inductive)) -- cgit v1.2.3 From bdfed9edf1e7ed929d1867442587c6ecef30986b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 16:07:52 +0100 Subject: Fix syntax highlighting of Module (Type). --- ide/coq.lang | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 1622e13330..2242ef1022 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,7 +29,7 @@ (\%{ident}\.)*\%{ident} [-+*{}] \.(\s|\z) - (Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion) + (Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion) (Hypothes[ie]s)|(Axiom(s)?)|(Variable(s)?)|(Parameter(s)?)|(Context)|(Implicit\%{space}+Type(s)?) (((Local)|(Global))\%{space}+)? (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property) @@ -190,6 +190,7 @@ Scheme\%{space}((Induction)|(Minimality)|(Elimination)|(Case)|(Equality))\%{space}for End Section + Module(\%{space}+Type)? Declare\%{space}+Module(\%{space}+((Import)|(Export)))? About Arguments -- cgit v1.2.3 From 29268d7e8e3c9925515c1e7aaaa77ae535e7f46e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 16:36:37 +0100 Subject: Fix syntax highlighting of Typeclasses Opaque. --- ide/coq.lang | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 2242ef1022..cfacd7ca43 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -205,7 +205,7 @@ (?'qua_list'(\%{space}+\%{qualit})+) - Typeclasses (Transparent)|(Opaque) + Typeclasses (Transparent|Opaque) Require(\%{space}+((Import)|(Export)))? Import Export -- cgit v1.2.3 From 0e9ad65b7302ae8fe419726e4a311e42e2dae749 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 16:51:10 +0100 Subject: Fix syntax highlighting of Extraction Language. --- ide/coq.lang | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index cfacd7ca43..fee84bd32e 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -164,6 +164,7 @@ \%{locality}Infix (Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist) Declare\%{space}+ML\%{space}+Module + Extraction\%{space}+Language\%{space}+(Ocaml|Haskell|Scheme) \%{locality}Hint\%{space}+ @@ -196,7 +197,7 @@ Arguments Implicit\%{space}+Arguments Include - (Recursive\%{space}+)?Extraction(\%{space}+(Language\%{space}+(Ocaml)|(Haskell)|(Scheme)|(Toplevel))|(Library)|((No)?Inline)|(Blacklist))? + (Recursive\%{space}+)?Extraction(\%{space}+((Library)|((No)?Inline)|(Blacklist)))? Extract\%{space}+((Inlined\%{space}+)?(Constant)|(Inductive)) -- cgit v1.2.3 From 1fe8a6717a51a616f97a3d5f130003301d64e963 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 16:57:20 +0100 Subject: Fix syntax highlighting of Extraction Inline and add Separate Extraction. --- ide/coq.lang | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index fee84bd32e..e13a94aeac 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -197,7 +197,6 @@ Arguments Implicit\%{space}+Arguments Include - (Recursive\%{space}+)?Extraction(\%{space}+((Library)|((No)?Inline)|(Blacklist)))? Extract\%{space}+((Inlined\%{space}+)?(Constant)|(Inductive)) @@ -210,6 +209,7 @@ Require(\%{space}+((Import)|(Export)))? Import Export + ((Recursive|Separate)\%{space}+)?Extraction(\%{space}+(Library|(No)?Inline|Blacklist))? -- cgit v1.2.3 From e3fa5b386e18ad9327cf635f92a0160792b202c6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 17:09:51 +0100 Subject: Fix syntax highlighting of Print/Reset Extraction. --- ide/coq.lang | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index e13a94aeac..22f0e48dcd 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -156,13 +156,13 @@ Eval Load Undo + (Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist) Print Comments Solve\%{space}+Obligation ((Uns)|(S))et(\%{space}+\%{ident})+ (\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation \%{locality}Infix - (Print)|(Reset)\%{space}+Extraction\%{space}+(Inline)|(Blacklist) Declare\%{space}+ML\%{space}+Module Extraction\%{space}+Language\%{space}+(Ocaml|Haskell|Scheme) -- cgit v1.2.3 From 0b660db0a7d771ee8e165327cb954013bbc1a7c8 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 6 Mar 2015 17:16:33 +0100 Subject: Simplify grammar for syntax highlighting by removing extraneous parentheses. --- ide/coq.lang | 50 +++++++++++++++++++++++++------------------------- 1 file changed, 25 insertions(+), 25 deletions(-) (limited to 'ide') diff --git a/ide/coq.lang b/ide/coq.lang index 22f0e48dcd..38dabda506 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -22,19 +22,19 @@ - \s + \s+ [_\p{L}] [_\p{L}'\pN] \%{first_ident_char}\%{ident_char}* (\%{ident}\.)*\%{ident} [-+*{}] \.(\s|\z) - (Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Function)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Class)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Coercion) - (Hypothes[ie]s)|(Axiom(s)?)|(Variable(s)?)|(Parameter(s)?)|(Context)|(Implicit\%{space}+Type(s)?) - (((Local)|(Global))\%{space}+)? - (Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property) - (Qed)|(Defined)|(Admitted)|(Abort)|(Save) - ((?'gal'\%{locality}(Program\%{space}+)?(\%{single_decl}|\%{begin_proof}))\%{space}+(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}+\%{ident})*))|(?'gal2'Goal) + Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion + Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)? + ((Local|Global)\%{space})? + Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property + Qed|Defined|Admitted|Abort|Save + ((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal) "" @@ -112,7 +112,7 @@ - Proof(\%{dot_sep}|\%{space}+(using)|\%{space}+(with)) + Proof(\%{dot_sep}|\%{space}using|\%{space}with) \%{end_proof}\%{dot_sep} @@ -159,15 +159,15 @@ (Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist) Print Comments - Solve\%{space}+Obligation - ((Uns)|(S))et(\%{space}+\%{ident})+ - (\%{locality}|((Reserved)|(Tactic))\%{space}+)?Notation + Solve\%{space}Obligation + (Uns|S)et(\%{space}\%{ident})+ + (\%{locality}|(Reserved|Tactic)\%{space})?Notation \%{locality}Infix - Declare\%{space}+ML\%{space}+Module - Extraction\%{space}+Language\%{space}+(Ocaml|Haskell|Scheme) + Declare\%{space}ML\%{space}Module + Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme) - \%{locality}Hint\%{space}+ + \%{locality}Hint\%{space} Resolve Immediate Constructors @@ -178,38 +178,38 @@ Rewrite - \%{space}+Scope + \%{space}Scope \%{locality}Open \%{locality}Close Bind Delimit - \%{space}+(?'qua'\%{qualit}) + \%{space}(?'qua'\%{qualit}) Chapter - Combined\%{space}+Scheme - Scheme\%{space}((Induction)|(Minimality)|(Elimination)|(Case)|(Equality))\%{space}for + Combined\%{space}Scheme + Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for End Section - Module(\%{space}+Type)? - Declare\%{space}+Module(\%{space}+((Import)|(Export)))? + Module(\%{space}Type)? + Declare\%{space}Module(\%{space}(Import|Export))? About Arguments - Implicit\%{space}+Arguments + Implicit\%{space}Arguments Include - Extract\%{space}+((Inlined\%{space}+)?(Constant)|(Inductive)) + Extract\%{space}((Inlined\%{space})?Constant|Inductive) - (?'qua_list'(\%{space}+\%{qualit})+) + (?'qua_list'(\%{space}\%{qualit})+) Typeclasses (Transparent|Opaque) - Require(\%{space}+((Import)|(Export)))? + Require(\%{space}(Import|Export))? Import Export - ((Recursive|Separate)\%{space}+)?Extraction(\%{space}+(Library|(No)?Inline|Blacklist))? + ((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))? -- cgit v1.2.3 From a6dd74621a61f19625d661c3168510a8762b6b7a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Mar 2015 16:00:39 +0100 Subject: CoqIDE: do not lose tag on Qed ending focused proof --- ide/coqOps.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 1800cb8fe8..6f8305afe4 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -589,7 +589,7 @@ object(self) Doc.assign_tip_id document id; let topstack, _ = Doc.context document in self#exit_focus; - self#cleanup (Doc.cut_at document tip); + self#cleanup ~all:true (Doc.cut_at document tip); logger Pp.Notice msg; self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] @@ -651,7 +651,7 @@ object(self) Doc.find_id document (fun id { start;stop } -> until (Some id) start stop) with Not_found -> initial_state, Doc.focused document - method private cleanup seg = + method private cleanup ~all seg = if seg <> [] then begin let start = buffer#get_iter_at_mark (CList.last seg).start in let stop = buffer#get_iter_at_mark (CList.hd seg).stop in @@ -662,7 +662,7 @@ object(self) buffer#remove_tag Tags.Script.unjustified ~start ~stop; buffer#remove_tag Tags.Script.tooltip ~start ~stop; buffer#remove_tag Tags.Script.to_process ~start ~stop; - buffer#remove_tag Tags.Script.read_only ~start ~stop; + if all then buffer#remove_tag Tags.Script.read_only ~start ~stop; buffer#remove_tag Tags.Script.error ~start ~stop; buffer#remove_tag Tags.Script.error_bg ~start ~stop; buffer#move_mark ~where:start (`NAME "start_of_input") @@ -694,13 +694,13 @@ object(self) Coq.bind (Coq.edit_at to_id) (function | Good (CSig.Inl (* NewTip *) ()) -> if unfocus_needed then self#exit_focus; - self#cleanup (Doc.cut_at document to_id); + self#cleanup ~all:true (Doc.cut_at document to_id); conclusion () | Good (CSig.Inr (* Focus *) (stop_id,(start_id,tip))) -> if unfocus_needed then self#exit_focus; - self#cleanup (Doc.cut_at document tip); + self#cleanup ~all:true (Doc.cut_at document tip); self#enter_focus start_id stop_id; - self#cleanup (Doc.cut_at document to_id); + self#cleanup ~all:false (Doc.cut_at document to_id); conclusion () | Fail (safe_id, loc, msg) -> if loc <> None then messages#push Pp.Error "Fixme LOC"; -- cgit v1.2.3 From 1a477d10daa91aadc0ef940b2f6d290aa93f8e8e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Mar 2015 16:01:06 +0100 Subject: CoqIDE: restore module/proof name in info bar --- ide/coqide.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index c977879a7b..861689800c 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -530,7 +530,7 @@ let update_status sn = | None -> "" | Some n -> ", proving " ^ n in - display ("Ready"^ if current.nanoPG then ", [μPG]" else "" ^ path ^ name); + display ("Ready"^ (if current.nanoPG then ", [μPG]" else "") ^ path ^ name); Coq.return () in Coq.bind (Coq.status ~logger:sn.messages#push false) next -- cgit v1.2.3 From d26602693de76604648e24f103ba6aa5f80fb556 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 9 Mar 2015 18:45:36 +0100 Subject: CoqIDE: fix tag colors to support superposing unsafe and partial Admitted (like Qed) can be "partially executed", but is also unsafe. --- ide/coqOps.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 6f8305afe4..c6073d599d 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -363,7 +363,7 @@ object(self) else if has_flag sentence `ERROR then [error_bg] else if has_flag sentence `INCOMPLETE then [incomplete] else [processed]) @ - (if [ `UNSAFE ] = sentence.flags then [unjustified] else []) + (if has_flag sentence `UNSAFE then [unjustified] else []) in List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags; List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags -- cgit v1.2.3 From 106b002b8e2d45c8824b145f29f5680317de78c4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Mar 2015 17:33:14 +0100 Subject: CoqIDE: load first _CoqProject file found and notify the user --- ide/coqide.ml | 12 ++++++++---- ide/project_file.ml4 | 22 +++++++--------------- 2 files changed, 15 insertions(+), 19 deletions(-) (limited to 'ide') diff --git a/ide/coqide.ml b/ide/coqide.ml index 861689800c..87efd17d22 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -84,14 +84,15 @@ let pr_exit_status = function | _ -> " failed" let make_coqtop_args = function - |None -> !sup_args + |None -> "", !sup_args |Some the_file -> let get_args f = Project_file.args_from_project f !custom_project_files prefs.project_file_name in match prefs.read_project with - |Ignore_args -> !sup_args - |Append_args -> get_args the_file @ !sup_args + |Ignore_args -> "", !sup_args + |Append_args -> + let fname, args = get_args the_file in fname, args @ !sup_args |Subst_args -> get_args the_file (** Setting drag & drop on widgets *) @@ -120,7 +121,10 @@ let set_drag (w : GObj.drag_ops) = (** Session management *) let create_session f = - let ans = Session.create f (make_coqtop_args f) in + let project_file, args = make_coqtop_args f in + if project_file <> "" then + flash_info (Printf.sprintf "Reading options from %s" project_file); + let ans = Session.create f args in let _ = set_drag ans.script#drag in ans diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index 41dc1befa2..f7279f9cfe 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -182,29 +182,21 @@ let read_project_file f = (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f))) let args_from_project file project_files default_name = - let is_f = CUnix.same_file file in - let contains_file dir = - List.exists (fun x -> is_f (CUnix.correct_path x dir)) - in let build_cmd_line ml_inc i_inc r_inc args = List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args []))) in try - let (_,(_,(ml_inc,i_inc,r_inc),(args,_))) = - List.find (fun (dir,((v_files,_,_,_),_,_)) -> - contains_file dir v_files) project_files in - build_cmd_line ml_inc i_inc r_inc args - with Not_found -> + let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in + fname, build_cmd_line ml_inc i_inc r_inc args + with Failure _ -> let rec find_project_file dir = try + let fname = Filename.concat dir default_name in let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) = - read_project_file (Filename.concat dir default_name) in - if contains_file dir v_files - then build_cmd_line ml_inc i_inc r_inc args - else let newdir = Filename.dirname dir in - if dir = newdir then [] else find_project_file newdir + read_project_file fname in + fname, build_cmd_line ml_inc i_inc r_inc args with Sys_error s -> let newdir = Filename.dirname dir in - if dir = newdir then [] else find_project_file newdir + if dir = newdir then "",[] else find_project_file newdir in find_project_file (Filename.dirname file) -- cgit v1.2.3