diff options
| author | msozeau | 2007-02-16 19:17:27 +0000 |
|---|---|---|
| committer | msozeau | 2007-02-16 19:17:27 +0000 |
| commit | b9e27721e88872a93ec7ca91575304ce1496a0ef (patch) | |
| tree | 355b6e71179b8ace71691c22033874f6e7b6cae9 /ide | |
| parent | 481494be9f20d9c497e4d7ac108ae19bbaa53201 (diff) | |
Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9656 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq_commands.ml | 15 | ||||
| -rw-r--r-- | ide/highlight.mll | 9 |
2 files changed, 18 insertions, 6 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 4dde601113..a8edc40612 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -77,10 +77,17 @@ let commands = [ ["Module"; "Module Type"; "Mutual Inductive";]; - ["Notation";]; - ["Opaque";]; + ["Notation"; + "Next Obligation";]; + ["Opaque"; + "Obligations Tactic";]; ["Parameter"; - "Proof."]; + "Proof."; + "Program Definition"; + "Program Fixpoint"; + "Program Lemma"; + "Program Theorem"; + ]; ["Qed."; ]; ["Read Module"; @@ -155,6 +162,8 @@ let state_preserving = [ "Extraction Module"; "Inspect"; "Locate"; + + "Obligations"; "Print"; "Print All."; "Print Classes"; diff --git a/ide/highlight.mll b/ide/highlight.mll index ea2f5bca4c..c033a6af5e 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -28,7 +28,8 @@ "Notation"; "Proof" ; "Print"; "Qed" ; "Require" ; "Reset"; "Undo"; "Save" ; "Section" ; "Unset" ; - "Set" ; "Notation" + "Set" ; "Notation"; + "Implicit"; "Arguments"; "Unfold"; "Resolve" ]; Hashtbl.mem h @@ -36,7 +37,7 @@ let h = Hashtbl.create 97 in List.iter (fun s -> Hashtbl.add h s ()) [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; - "end"; "as"; "let"; "if"; "then"; "else"; "return"; + "end"; "as"; "let"; "in"; "dest"; "if"; "then"; "else"; "return"; "Prop"; "Set"; "Type"]; Hashtbl.mem h @@ -45,7 +46,7 @@ List.iter (fun s -> Hashtbl.add h s ()) [ "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ; "Proposition" ; "Property" ; "Definition" ; "Let" ; "Example" ; "SubClass" ; "Inductive" ; "CoInductive" ; - "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint"; + "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint"; "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ; "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters" ]; @@ -74,12 +75,14 @@ let declaration = "Inductive" | "CoInductive" | "Record" | "Structure" | "Fixpoint" | "CoFixpoint" + rule next_order = parse | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf } | "Module Type" { lexeme_start lexbuf, lexeme_end lexbuf, "kwd" } + | "Program" space+ ident as id { lexeme_start lexbuf, lexeme_end lexbuf, "decl" } | ident as id { if is_keyword id then lexeme_start lexbuf, lexeme_end lexbuf, "kwd" |