diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-02 17:11:21 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-02 17:11:21 +0000 |
commit | 04d66a258efb91e73c313b3315abd2810947028d (patch) | |
tree | 33b1fb09b046b493783ea31e9c4aec5698697880 | |
parent | 7940eba979f8a64da7c89e69659777d1b65d67f3 (diff) |
Coqide coq lexer put one tag at the end of a sentence.
And that's all !
It erase the possibility of code folding...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15268 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | ide/coq_lex.mll | 142 | ||||
-rw-r--r-- | ide/coqide.ml | 43 | ||||
-rw-r--r-- | ide/coqide_ui.ml | 2 | ||||
-rw-r--r-- | ide/tags.ml | 9 | ||||
-rw-r--r-- | ide/tags.mli | 9 |
5 files changed, 31 insertions, 174 deletions
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index c9a9a8260..fbcbbd788 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -7,129 +7,32 @@ (************************************************************************) { - open Lexing - - type token = - | Comment - | Keyword - | Declaration - | ProofDeclaration - | Qed - | String - - (* Without this table, the automaton would be too big and - ocamllex would fail *) - - let tag_of_ident = - let one_word_commands = - [ "Add" ; "Check"; "Eval"; "Extraction" ; - "Load" ; "Undo"; "Goal"; - "Proof" ; "Print";"Save" ; "Restart"; - "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ] - in - let one_word_declarations = - [ (* 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" ; "Instance"; "Include"; "Context"; "Class" ; - "Arguments" ] - in - let proof_declarations = - [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ; - "Proposition" ; "Property" ] - in - let proof_ends = - [ "Qed" ; "Defined" ; "Admitted"; "Abort" ] - in - let constr_keywords = - [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; - "end"; "as"; "let"; "in"; "if"; "then"; "else"; "return"; - "Prop"; "Set"; "Type" ] - in - let h = Hashtbl.create 97 in (* for vernac *) - let h' = Hashtbl.create 97 in (* for constr *) - List.iter (fun s -> Hashtbl.add h s Keyword) one_word_commands; - List.iter (fun s -> Hashtbl.add h s Declaration) one_word_declarations; - List.iter (fun s -> Hashtbl.add h s ProofDeclaration) proof_declarations; - List.iter (fun s -> Hashtbl.add h s Qed) proof_ends; - List.iter (fun s -> Hashtbl.add h' s Keyword) constr_keywords; - (fun initial id -> Hashtbl.find (if initial then h else h') id) - exception Unterminated - - let here f lexbuf = f (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) - } let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *) -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 undotted_sep = [ '{' '}' '-' '+' '*' ] let dot_sep = '.' (space | eof) -let multiword_declaration = - "Module" (space+ "Type")? -| "Program" space+ ident -| "Existing" space+ "Instance" "s"? -| "Canonical" space+ "Structure" - -let locality = (space+ "Local")? - -let multiword_command = - ("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")? -| "Hint" locality space+ ident -| "Reset" (space+ "Initial")? -| "Tactic" space+ "Notation" -| "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, ... *) - rule coq_string = parse - | "\"\"" { coq_string lexbuf } - | "\"" { Lexing.lexeme_end lexbuf } - | eof { Lexing.lexeme_end lexbuf } + | "\\\"" { coq_string lexbuf } + | "\"" { () } + | eof { () } | _ { coq_string lexbuf } and comment = parse | "(*" { ignore (comment lexbuf); comment lexbuf } - | "\"" { ignore (coq_string lexbuf); comment lexbuf } + | "\"" { let () = coq_string lexbuf in comment lexbuf } | "*)" { (true, Lexing.lexeme_start lexbuf + 2) } | eof { (false, Lexing.lexeme_end lexbuf) } | _ { comment lexbuf } -and sentence initial stamp = parse +and sentence initial = parse | "(*" { - let comm_start = Lexing.lexeme_start lexbuf in let trully_terminated,comm_end = comment lexbuf in - stamp comm_start comm_end Comment; if not trully_terminated then raise Unterminated; (* A comment alone is a sentence. A comment in a sentence doesn't terminate the sentence. @@ -137,47 +40,34 @@ and sentence initial stamp = parse as required when tagging a zone, hence the -1 to locate the ")" terminating the comment. *) - if initial then comm_end - 1 else sentence false stamp lexbuf + if initial then true, comm_end - 1 else sentence false lexbuf } | "\"" { - let str_start = Lexing.lexeme_start lexbuf in - let str_end = coq_string lexbuf in - stamp str_start str_end String; - sentence false stamp lexbuf - } - | multiword_declaration { - if initial then here stamp lexbuf Declaration; - sentence false stamp lexbuf - } - | multiword_command { - if initial then here stamp lexbuf Keyword; - sentence false stamp lexbuf + let () = coq_string lexbuf in + sentence false lexbuf } - | ident as id { - (try here stamp lexbuf (tag_of_ident initial id) with Not_found -> ()); - sentence false stamp lexbuf } | ".." { (* We must have a particular rule for parsing "..", where no dot is a terminator, even if we have a blank afterwards (cf. for instance the syntax for recursive notation). This rule and the following one also allow to treat the "..." special case, where the third dot is a terminator. *) - sentence false stamp lexbuf + sentence false lexbuf } - | dot_sep { Lexing.lexeme_start lexbuf } (* The usual "." terminator *) + | dot_sep { false, Lexing.lexeme_start lexbuf } (* The usual "." terminator *) | undotted_sep { (* Separators like { or } and bullets * - + are only active at the start of a sentence *) - if initial then Lexing.lexeme_start lexbuf - else sentence false stamp lexbuf + if initial then false, Lexing.lexeme_start lexbuf + else sentence false lexbuf } | space+ { (* Parsing spaces is the only situation preserving initiality *) - sentence initial stamp lexbuf + sentence initial lexbuf } | _ { (* Any other characters *) - sentence false stamp lexbuf + sentence false lexbuf } | eof { raise Unterminated } @@ -189,7 +79,7 @@ and sentence initial stamp = parse It will raise [Unterminated] when no end of sentence is found. *) - let delimit_sentence stamp slice = - sentence true stamp (Lexing.from_string slice) + let delimit_sentence slice = + sentence true (Lexing.from_string slice) } diff --git a/ide/coqide.ml b/ide/coqide.ml index 429c4c334..b94f09053 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -392,43 +392,23 @@ let with_file handler name ~f = (* For find_phrase_starting_at *) exception Stop of int -let tag_of_sort = function - | Coq_lex.Comment -> Tags.Script.comment - | Coq_lex.Keyword -> Tags.Script.kwd - | Coq_lex.Declaration -> Tags.Script.decl - | Coq_lex.ProofDeclaration -> Tags.Script.proof_decl - | Coq_lex.Qed -> Tags.Script.qed - | Coq_lex.String -> failwith "No tag" - -let apply_tag (buffer:GText.buffer) orig off_conv from upto sort = - try - let tag = tag_of_sort sort in - let start = orig#forward_chars (off_conv from) in - let stop = orig#forward_chars (off_conv upto) in - buffer#apply_tag ~start ~stop tag - with _ -> () - -let remove_tags (buffer:GText.buffer) from upto = - List.iter (buffer#remove_tag ~start:from ~stop:upto) - [ Tags.Script.comment; Tags.Script.kwd; Tags.Script.decl; - Tags.Script.proof_decl; Tags.Script.qed ] - (** Cut a part of the buffer in sentences and tag them. May raise [Coq_lex.Unterminated] when the zone ends with an unterminated sentence. *) let split_slice_lax (buffer:GText.buffer) from upto = - remove_tags buffer from upto; + buffer#remove_tag ~start:from ~stop:upto Tags.Script.comment_sentence; buffer#remove_tag ~start:from ~stop:upto Tags.Script.sentence; let slice = buffer#get_text ~start:from ~stop:upto () in let rec split_substring str = let off_conv = byte_offset_to_char_offset str in let slice_len = String.length str in - let end_off = Coq_lex.delimit_sentence (apply_tag buffer from off_conv) str + let is_comment,end_off = Coq_lex.delimit_sentence str in let start = from#forward_chars (off_conv end_off) in let stop = start#forward_char in - buffer#apply_tag ~start ~stop Tags.Script.sentence; + buffer#apply_tag ~start ~stop + (if is_comment then Tags.Script.comment_sentence else Tags.Script.sentence); let next = end_off + 1 in if next < slice_len then begin ignore (from#nocopy#forward_chars (off_conv next)); @@ -447,7 +427,7 @@ let rec backward_search cond (iter:GText.iter) = if iter#is_start || cond iter then iter else backward_search cond iter#backward_char -let is_sentence_end s = s#has_tag Tags.Script.sentence +let is_sentence_end s = s#has_tag Tags.Script.sentence || s#has_tag Tags.Script.comment_sentence let is_char s c = s#char = Char.code c (** Search backward the first character of a sentence, starting at [iter] @@ -508,6 +488,7 @@ let force_retag buffer = try split_slice_lax buffer buffer#start_iter buffer#end_iter with Coq_lex.Unterminated -> () +(* GtkSource view should handle that one day !!! let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) = (* move back twice if not into proof_decl, * once if into proof_decl and back_char into_proof_decl, @@ -527,6 +508,7 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) = else ( buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) +*) (** The arguments that will be passed to coqtop. No quoting here, since no /bin/sh when using create_process instead of open_process. *) @@ -939,7 +921,7 @@ object(self) match sync get_next_phrase () with | None -> raise Unsuccessful | Some ((_,stop) as loc,phrase) -> - if stop#backward_char#has_tag Tags.Script.comment + if stop#backward_char#has_tag Tags.Script.comment_sentence then sync mark_processed Safe loc else try match self#send_to_coq ct verbosely phrase true true true with | Some safe -> sync mark_processed safe loc @@ -1085,7 +1067,7 @@ object(self) else let phrase = Stack.pop cmd_stack in let stop = input_buffer#get_iter_at_mark phrase.stop in - if stop#backward_char#has_tag Tags.Script.comment + if stop#backward_char#has_tag Tags.Script.comment_sentence then n_pop n else n_pop (pred n) in @@ -1120,7 +1102,7 @@ object(self) if i#compare stop >= 0 then n else begin ignore (Stack.pop cmd_stack); - if stop#backward_char#has_tag Tags.Script.comment + if stop#backward_char#has_tag Tags.Script.comment_sentence then n_step n else n_step (succ n) end @@ -1158,7 +1140,7 @@ object(self) let phrase = Stack.pop cmd_stack in let stop = input_buffer#get_iter_at_mark phrase.stop in let count = - if stop#backward_char#has_tag Tags.Script.comment then 0 else 1 + if stop#backward_char#has_tag Tags.Script.comment_sentence then 0 else 1 in let finish where = input_buffer#place_cursor ~where; @@ -2225,11 +2207,12 @@ let main files = GAction.add_action "Interrupt" ~label:"_Interrupt" ~stock:`STOP ~callback:(fun _ -> break ()) ~tooltip:"Interrupt computations" ~accel:(!current.modifier_for_navigation^"Break"); +(* wait for this available in GtkSourceView ! GAction.add_action "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE ~callback:(fun _ -> let sess = session_notebook#current_term in toggle_proof_visibility sess.script#buffer sess.analyzed_view#get_insert) ~tooltip:"Hide proof" - ~accel:(!current.modifier_for_navigation^"h"); + ~accel:(!current.modifier_for_navigation^"h");*) GAction.add_action "Previous" ~label:"_Previous" ~stock:`GO_BACK ~callback:(fun _ -> do_or_activate (fun a -> a#go_to_prev_occ_of_cur_word) ()) ~tooltip:"Previous occurence" ~accel:(!current.modifier_for_navigation^"less"); diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 6b464348c..adfd9e668 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -82,7 +82,6 @@ let init () = <menuitem action='Start' /> <menuitem action='End' /> <menuitem action='Interrupt' /> - <menuitem action='Hide' /> <menuitem action='Previous' /> <menuitem action='Next' /> </menu> @@ -145,7 +144,6 @@ let init () = <toolitem action='Start' /> <toolitem action='End' /> <toolitem action='Interrupt' /> - <toolitem action='Hide' /> <toolitem action='Previous' /> <toolitem action='Next' /> <toolitem action='Wizard' /> diff --git a/ide/tags.ml b/ide/tags.ml index db1549e78..14a04f359 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -19,19 +19,12 @@ let processing_color = ref "light blue" module Script = struct let table = GText.tag_table () - let kwd = make_tag table ~name:"kwd" [`FOREGROUND "blue"] - let qed = make_tag table ~name:"qed" [`FOREGROUND "blue"] - let decl = make_tag table ~name:"decl" [`FOREGROUND "orange red"] - let proof_decl = make_tag table ~name:"proof_decl" [`FOREGROUND "orange red"] - let comment = make_tag table ~name:"comment" [`FOREGROUND "brown"] - let reserved = make_tag table ~name:"reserved" [`FOREGROUND "dark red"] + let comment_sentence = make_tag table ~name:"comment_sentence" [] let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"] let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color ;`EDITABLE false] let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color;`EDITABLE false] let unjustified = make_tag table ~name:"unjustified" [`UNDERLINE `SINGLE; `FOREGROUND "red"; `BACKGROUND "gold";`EDITABLE false] let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"] - let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false] - let folded = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"] let sentence = make_tag table ~name:"sentence" [] end module Proof = diff --git a/ide/tags.mli b/ide/tags.mli index 5a5356193..b51e85e25 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -9,19 +9,12 @@ module Script : sig val table : GText.tag_table - val kwd : GText.tag - val qed : GText.tag - val decl : GText.tag - val proof_decl : GText.tag - val comment : GText.tag - val reserved : GText.tag + val comment_sentence : GText.tag val error : GText.tag val to_process : GText.tag val processed : GText.tag val unjustified : GText.tag val found : GText.tag - val hidden : GText.tag - val folded : GText.tag val sentence : GText.tag end |