diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-12 20:49:05 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-12 20:49:05 +0000 |
commit | 8d0136caf2458c2a2457550b1af1299098b1d038 (patch) | |
tree | 2d16c2661a33616797657b4c919de84c1a624601 /ide/coq_lex.mll | |
parent | 59c9403ceb09a35ed219b522e9f5abdb50615d76 (diff) |
Coqide minor enhancements
Bug 2736: Syntax highlighting
600 transitions left before ocamllex limit.
A preference pane large enough to change fonts.
Erase extra empty line in Coqide goal display.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15145 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq_lex.mll')
-rw-r--r-- | ide/coq_lex.mll | 26 |
1 files changed, 11 insertions, 15 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 314e15e3e..c9a9a8260 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -37,7 +37,8 @@ (* Inductive *) "Inductive" ; "CoInductive" ; "Record" ; "Structure" ; (* Other *) - "Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class" ] + "Ltac" ; "Instance"; "Include"; "Context"; "Class" ; + "Arguments" ] in let proof_declarations = [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ; @@ -85,33 +86,28 @@ let multiword_declaration = | "Existing" space+ "Instance" "s"? | "Canonical" space+ "Structure" -let locality = ("Local" space+)? +let locality = (space+ "Local")? let multiword_command = - "Set" (space+ ident)* -| "Unset" (space+ ident)* -| "Open" space+ locality "Scope" -| "Close" space+ locality "Scope" -| "Bind" space+ "Scope" -| "Arguments" space+ "Scope" -| "Reserved" space+ "Notation" space+ locality -| "Delimit" space+ "Scope" + ("Uns" | "S")" et" (space+ ident)* +| (("Open" | "Close") locality | "Bind" | " Delimit" ) + space+ "Scope" +| (("Reserved" space+)? "Notation" | "Infix") locality space+ | "Next" space+ "Obligation" | "Solve" space+ "Obligations" | "Require" space+ ("Import"|"Export")? -| "Infix" space+ locality -| "Notation" space+ locality -| "Hint" space+ locality ident +| "Hint" locality space+ ident | "Reset" (space+ "Initial")? | "Tactic" space+ "Notation" -| "Implicit" space+ "Arguments" -| "Implicit" space+ ("Type"|"Types") +| "Implicit" space+ "Type" "s"? | "Combined" space+ "Scheme" | "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"|"Toplevel"))| ("Library"|"Inline"|"NoInline"|"Blacklist")) | "Recursive" space+ "Extraction" (space+ "Library")? | ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist") | "Extract" space+ (("Inlined" space+) "Constant"| "Inductive") +| "Typeclasses" space+ ("eauto" | "Transparent" | "Opaque") +| ("Generalizable" space+) ("All" | "No")? "Variable" "s"? (* At least still missing: "Inline" + decl, variants of "Identity Coercion", variants of Print, Add, ... *) |