diff options
author | 2009-11-13 13:36:12 +0000 | |
---|---|---|
committer | 2009-11-13 13:36:12 +0000 | |
commit | ed7ec57e326284e449d3170cd2c0a6ba6a5a6d92 (patch) | |
tree | ab83a9033e76314ab6f9f42f6ea89c46b1aabfba /ide | |
parent | 4f4c8cdf837763ab8ebc5988f37b8b63f8a284e3 (diff) |
lexing refactoring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12516 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r-- | ide/syntaxBlocks.mll | 60 | ||||
-rw-r--r-- | ide/syntaxTokens.mll | 158 |
2 files changed, 218 insertions, 0 deletions
diff --git a/ide/syntaxBlocks.mll b/ide/syntaxBlocks.mll new file mode 100644 index 000000000..415ef6359 --- /dev/null +++ b/ide/syntaxBlocks.mll @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +{ +type markup = + | Comment of (int*int) + | String of (int*int) + | SentenceEnd of int + +} + +let ws = [' ' '\010' '\013' '\009' '\012'] + +let sentence_sep = '.' [ ' ' '\n' '\t'] + +rule coq_string = parse + | "\"\"" { coq_string lexbuf } + | "\"" { Lexing.lexeme_end lexbuf } + | _ { coq_string lexbuf } + | eof { Lexing.lexeme_end lexbuf } + +and comment = parse + | "(*" { ignore (comment lexbuf); comment lexbuf } + | "*)" { Lexing.lexeme_end lexbuf } + | "\"" { ignore (coq_string lexbuf); comment lexbuf } + | _ { comment lexbuf } + | eof { Lexing.lexeme_end lexbuf } + +and sentence tag_cb = parse + | ws+ { sentence tag_cb lexbuf } + | _ { sentence tag_cb lexbuf } + | ".." { sentence tag_cb lexbuf } + | "(*" { + let comm_start = Lexing.lexeme_start lexbuf in + let comm_end = comment lexbuf in + tag_cb (Comment (comm_start,comm_end)); + sentence tag_cb lexbuf } + | "\"" { + let str_start = Lexing.lexeme_start lexbuf in + let str_end = coq_string lexbuf in + tag_cb (String (str_start,str_end)); + sentence tag_cb lexbuf } + | eof { raise Not_found } + | sentence_sep { + tag_cb (SentenceEnd (Lexing.lexeme_end lexbuf)) + } + +{ + let parse tag_cb slice = + let lb = Lexing.from_string slice in + sentence tag_cb lb; + Lexing.lexeme_end lb +} diff --git a/ide/syntaxTokens.mll b/ide/syntaxTokens.mll new file mode 100644 index 000000000..1939d801d --- /dev/null +++ b/ide/syntaxTokens.mll @@ -0,0 +1,158 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +{ + open Lexing + + type markup = + | Keyword of (int*int) + | Declaration of (int*int) + + (* Without this table, the automaton would be too big and + ocamllex would fail *) + let is_one_word_command = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "Add" ; "Check"; "Eval"; "Extraction" ; + "Load" ; "Undo"; "Goal"; + "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ; + "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" + ]; + Hashtbl.mem h + + let is_constr_kw = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; + "end"; "as"; "let"; "in"; "if"; "then"; "else"; "return"; + "Prop"; "Set"; "Type" ]; + Hashtbl.mem h + + (* Without this table, the automaton would be too big and + ocamllex would fail *) + let is_one_word_declaration = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ (* Theorems *) + "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ; + "Proposition" ; "Property" ; + (* Definitions *) + "Definition" ; "Let" ; "Example" ; "SubClass" ; + "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ; + (* Assumptions *) + "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ; + "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters"; + (* Inductive *) + "Inductive" ; "CoInductive" ; "Record" ; "Structure" ; + (* Other *) + "Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class" + ]; + Hashtbl.mem h + + let starting = ref true +} + +let space = + [' ' '\010' '\013' '\009' '\012'] +let firstchar = + ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'] +let identchar = + ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] +let ident = firstchar identchar* + +let multiword_declaration = + "Module" (space+ "Type")? +| "Program" space+ ident +| "Existing" space+ "Instance" +| "Canonical" space+ "Structure" + +let locality = ("Local" space+)? + +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" +| "Next" space+ "Obligation" +| "Solve" space+ "Obligations" +| "Require" space+ ("Import"|"Export")? +| "Infix" space+ locality +| "Notation" space+ locality +| "Hint" space+ locality ident +| "Reset" (space+ "Initial")? +| "Tactic" space+ "Notation" +| "Implicit" space+ "Arguments" +| "Implicit" space+ ("Type"|"Types") +| "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") + +(* At least still missing: "Inline" + decl, variants of "Identity + Coercion", variants of Print, Add, ... *) + +rule coq_string = parse + | "\"\"" { coq_string lexbuf } + | "\"" { } + | _ { coq_string lexbuf } + | eof { } + +and comment = parse + | "(*" { comment lexbuf; comment lexbuf } + | "*)" { } + | "\"" { coq_string lexbuf; comment lexbuf } + | _ { comment lexbuf } + | eof { } + +and sentence tag_cb = parse + | "(*" { comment lexbuf; sentence tag_cb lexbuf } + | "\"" { coq_string lexbuf; start := false; sentence tag_cb lexbuf } + | space+ { sentence tag_cb lexbuf } + | multiword_declaration { + if !start then begin + start := false; + tag_cb Declaration (lexeme_start lexbuf) (lexeme_end lexbuf) + end; + inside_sentence lexbuf } + | multiword_command { + if !start then begin + start := false; + tag_cb Keyword (lexeme_start lexbuf) (lexeme_end lexbuf) + end; + sentence tag_cb lexbuf } + | ident as id { + if !start then begin + start := false; + if id <> "Time" then begin + if is_one_word_command id then + tag_cb Keyword (lexeme_start lexbuf) (lexeme_end lexbuf) + else if is_one_word_declaration id then + tag_cb Declaration (lexeme_start lexbuf) (lexeme_end lexbuf) + end + end else begin + if is_constr_kw id then + tag_cb Keyword (lexeme_start lexbuf) (lexeme_end lexbuf); + end; + sentence tag_cb lexbuf } + | _ { sentence tag_cb lexbuf} + | eof { } + +{ + let parse tag_cb slice = + let lb = from_string slice in + start := true; + sentence tag_cb lb +} |