From 3cf7a09799982924453df29b3bb4d081a0e089b4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 26 Apr 2015 21:51:49 +0200
Subject: Open the file chooser even if there is no current session. (Fix bug
#4206)
---
ide/coqide.ml | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
(limited to 'ide')
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0f4cb7b073..c0e2281258 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -253,14 +253,14 @@ let newfile _ =
!refresh_editor_hook ();
notebook#goto_page index
-let load sn =
- let filename = sn.fileops#filename in
+let load _ =
+ let filename =
+ try notebook#current_term.fileops#filename
+ with Invalid_argument _ -> None in
match select_file_for_open ~title:"Load file" ?filename () with
| None -> ()
| Some f -> FileAux.load_file f
-let load = cb_on_current_term load
-
let save _ = on_current_term (FileAux.check_save ~saveas:false)
let saveas sn =
--
cgit v1.2.3
From 5fc6e3a9e8fdd81be83194bbd62093993ddd4b01 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 27 Apr 2015 23:03:41 +0200
Subject: Improve syntax highlighting.
- Arithmetic operators and brackets are no longer recognized as bullets,
unless they follow a stop or start a line.
- Most vernacular commands are no longer highlighted when used inside
proof scripts.
- Coqdoc comments now take precedence over regular comments.
---
ide/coq.lang | 360 ++++++++++++++++++++++++++++++-----------------------------
1 file changed, 186 insertions(+), 174 deletions(-)
(limited to 'ide')
diff --git a/ide/coq.lang b/ide/coq.lang
index 65150d6a95..35dff85e62 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -5,7 +5,7 @@
\(\*
\*\)
-
+
@@ -20,15 +20,15 @@
-
+
\s+
[_\p{L}]
[_\p{L}'\pN]
\%{first_ident_char}\%{ident_char}*
(\%{ident}\.)*\%{ident}
- [-+*{}]
\.(\s|\z)
+ ([-+*]+|{)(\s|\z)|}(\s*})*
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})?
@@ -36,185 +36,197 @@
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)
-
- ""
-
-
+
+
"
"
-
+
+ ""
+
+
+
+
+
+
+
+
+
+
+
+
+ forall
+ fun
+ match
+ fix
+ cofix
+ with
+ for
+ end
+ as
+ let
+ in
+ if
+ then
+ else
+ return
+
+
+
+
+ Prop
+ Set
+ Type
+
+
-
- \(\*\*(\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(\%{dot_sep}|\%{space}using|\%{space}with)
- \%{end_proof}\%{dot_sep}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- \b[^-+*{}]
- \%{dot_sep}
-
-
-
-
-
-
-
-
-
- Proof
- \%{dot_sep}
-
-
-
-
-
-
-
- \%{undotted_sep}
-
-
- Add
- Check
- 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
- Declare\%{space}ML\%{space}Module
- Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)
-
-
- \%{locality}Hint\%{space}
- Resolve
- Immediate
- Constructors
- Unfold
- Opaque
- Transparent
- Extern
- Rewrite
-
-
- \%{space}Scope
- \%{locality}Open
- \%{locality}Close
- Bind
- Delimit
-
-
- \%{space}(?'qua'\%{qualit})
- Chapter
- Combined\%{space}Scheme
- Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for
- End
- Section
- Module(\%{space}Type)?
- Declare\%{space}Module(\%{space}(Import|Export))?
- About
- Arguments
- Implicit\%{space}Arguments
- Include
- Extract\%{space}((Inlined\%{space})?Constant|Inductive)
-
-
-
-
-
-
- (?'qua_list'(\%{space}\%{qualit})+)
- Typeclasses (Transparent|Opaque)
- Require(\%{space}(Import|Export))?
- Import
- Export
- ((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?
-
-
-
-
-
+
+
+
+
+ \%{decl_head}
+ \%{dot_sep}
+
+
+
+
+
+
+
+
+
+ \.\.
+
+
+
+
+
+
+
+
+ Proof(\%{dot_sep}|\%{space}using|\%{space}with)
+ \%{end_proof}\%{dot_sep}
+
+
+
+
+
+
+
+
+
+
+ \%{dot_sep}\s*(?'bul'\%{bullet})
+
+
+
+
+
+ ^\s*\%{bullet}
+
+
+
+
+
+ Proof
+ \%{dot_sep}
+
+
+
+
+
+
+
+
+ About
+ Check
+ Print
+ Eval
+ Undo
+ Opaque
+ Transparent
+
+
+
+ Add
+ Load
+ (Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)
+ Comments
+ 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|JSON)
+
+
+
+ \%{locality}Hint\%{space}
+ Resolve
+ Immediate
+ Constructors
+ Unfold
+ Extern
+ Rewrite
+
+
+
+ \%{space}Scope
+ \%{locality}Open
+ \%{locality}Close
+ Bind
+ Delimit
+
+
+
+ \%{space}(?'qua'\%{qualit})
+ Chapter
+ Combined\%{space}Scheme
+ Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for
+ End
+ Section
+ Module(\%{space}Type)?
+ Declare\%{space}Module(\%{space}(Import|Export))?
+ Arguments
+ Implicit\%{space}Arguments
+ Include
+ Extract\%{space}((Inlined\%{space})?Constant|Inductive)
+
+
+
+
+
+
+
+ (?'qua_list'(\%{space}\%{qualit})+)
+ Typeclasses (Transparent|Opaque)
+ Require(\%{space}(Import|Export))?
+ Import
+ Export
+ ((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?
+
+
+
+
+
--
cgit v1.2.3