diff options
-rw-r--r-- | ide/coqLex.mll (renamed from ide/syntaxTokens.mll) | 102 | ||||
-rw-r--r-- | ide/coqide.ml | 168 | ||||
-rw-r--r-- | ide/ide.mllib | 2 | ||||
-rw-r--r-- | ide/syntaxBlocks.mll | 60 | ||||
-rw-r--r-- | ide/tags.ml | 5 |
5 files changed, 175 insertions, 162 deletions
diff --git a/ide/syntaxTokens.mll b/ide/coqLex.mll index 1939d801d..03ce950fd 100644 --- a/ide/syntaxTokens.mll +++ b/ide/coqLex.mll @@ -11,9 +11,13 @@ { open Lexing - type markup = - | Keyword of (int*int) - | Declaration of (int*int) + type token = + | Comment + | Keyword + | Declaration + | ProofDeclaration + | Qed + | String (* Without this table, the automaton would be too big and ocamllex would fail *) @@ -22,7 +26,7 @@ List.iter (fun s -> Hashtbl.add h s ()) [ "Add" ; "Check"; "Eval"; "Extraction" ; "Load" ; "Undo"; "Goal"; - "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ; + "Proof" ; "Print";"Save" ; "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]; Hashtbl.mem h @@ -40,10 +44,7 @@ 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 *) + [ (* Definitions *) "Definition" ; "Let" ; "Example" ; "SubClass" ; "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ; (* Assumptions *) @@ -56,17 +57,33 @@ ]; Hashtbl.mem h - let starting = ref true + let is_proof_declaration = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ; + "Proposition" ; "Property" ]; + Hashtbl.mem h + + let is_proof_end = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "Qed" ; "Defined" ; "Admitted" ]; + Hashtbl.mem h + + let start = 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 sentence_sep = '.' [ ' ' '\n' '\t' ] + let multiword_declaration = "Module" (space+ "Type")? | "Program" space+ ident @@ -106,53 +123,72 @@ let multiword_command = rule coq_string = parse | "\"\"" { coq_string lexbuf } - | "\"" { } + | "\"" { Lexing.lexeme_end lexbuf } + | eof { Lexing.lexeme_end lexbuf } | _ { coq_string lexbuf } - | eof { } and comment = parse - | "(*" { comment lexbuf; comment lexbuf } - | "*)" { } - | "\"" { coq_string lexbuf; comment lexbuf } + | "(*" { ignore (comment lexbuf); comment lexbuf } + | "\"" { ignore (coq_string lexbuf); comment lexbuf } + | "*)" { Lexing.lexeme_end lexbuf } + | eof { Lexing.lexeme_end 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 } +and sentence stamp = parse + | space+ { sentence stamp lexbuf } + | "(*" { + let comm_start = Lexing.lexeme_start lexbuf in + let comm_end = comment lexbuf in + stamp comm_start comm_end Comment; + sentence stamp lexbuf + } + | "\"" { + let str_start = Lexing.lexeme_start lexbuf in + let str_end = coq_string lexbuf in + stamp str_start str_end String; + start := false; + sentence stamp lexbuf + } | multiword_declaration { if !start then begin start := false; - tag_cb Declaration (lexeme_start lexbuf) (lexeme_end lexbuf) + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration end; - inside_sentence lexbuf } + sentence stamp lexbuf + } | multiword_command { if !start then begin start := false; - tag_cb Keyword (lexeme_start lexbuf) (lexeme_end lexbuf) + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword end; - sentence tag_cb lexbuf } + sentence stamp 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) + if is_proof_end id then + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Qed + else if is_one_word_command id then + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword else if is_one_word_declaration id then - tag_cb Declaration (lexeme_start lexbuf) (lexeme_end lexbuf) + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration + else if is_proof_declaration id then + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) ProofDeclaration end end else begin if is_constr_kw id then - tag_cb Keyword (lexeme_start lexbuf) (lexeme_end lexbuf); + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword end; - sentence tag_cb lexbuf } - | _ { sentence tag_cb lexbuf} - | eof { } + sentence stamp lexbuf } + | ".." + | _ { sentence stamp lexbuf} + | sentence_sep { } + | eof { raise Not_found } { - let parse tag_cb slice = - let lb = from_string slice in + let find_end_offset stamp slice = + let lb = Lexing.from_string slice in start := true; - sentence tag_cb lb + sentence stamp lb; + Lexing.lexeme_end lb } diff --git a/ide/coqide.ml b/ide/coqide.ml index fb7b92d71..f74d63051 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -96,10 +96,6 @@ object('self) method undo_last_step : unit method help_for_keyword : unit -> unit method complete_at_offset : int -> bool - - method toggle_proof_visibility : GText.iter -> unit - method hide_proof : GText.iter -> GText.iter -> GText.iter -> unit - method unhide_proof : GText.iter -> GText.iter -> GText.iter -> unit end @@ -522,6 +518,98 @@ let warning msg = img#coerce) msg +let apply_tag (buffer:GText.buffer) orig off_conv from upto sort = + let conv_and_apply start stop tag = + let start = orig#forward_chars (off_conv from) in + let stop = orig#forward_chars (off_conv upto) in + buffer#apply_tag ~start ~stop tag + in match sort with + | CoqLex.Comment -> + conv_and_apply from upto Tags.Script.comment + | CoqLex.Keyword -> + conv_and_apply from upto Tags.Script.kwd + | CoqLex.Declaration -> + conv_and_apply from upto Tags.Script.decl + | CoqLex.ProofDeclaration -> + conv_and_apply from upto Tags.Script.proof_decl + | CoqLex.Qed -> + conv_and_apply from upto Tags.Script.qed + | CoqLex.String -> () + +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; Tags.Script.sentence_end ] + +let tag_slice (buffer:GText.buffer) from upto on_fail = + remove_tags buffer from upto; + buffer#remove_tag ~start:from ~stop:upto Tags.Script.sentence_end; + let slice = buffer#get_text ~start:from ~stop:upto () in + let rec tag_substring str = + let off_conv = byte_offset_to_char_offset str in + let slice_len = String.length str in + let tag_cnt = CoqLex.find_end_offset (apply_tag buffer from off_conv) str in + + let stop = from#forward_chars (off_conv tag_cnt) in + let start = stop#backward_char in + buffer#apply_tag ~start ~stop Tags.Script.sentence_end; + + if tag_cnt <> slice_len then begin + ignore (from#nocopy#forward_chars (off_conv tag_cnt)); + tag_substring (String.sub str tag_cnt (slice_len - tag_cnt)) + end + in + try tag_substring slice with Not_found -> on_fail buffer from upto + +let get_sentence_bounds (iter:GText.iter) = + let start = iter#backward_to_tag_toggle (Some Tags.Script.sentence_end) in + (if start#has_tag Tags.Script.sentence_end then ignore ( + start#nocopy#forward_to_tag_toggle (Some Tags.Script.sentence_end))); + let stop = start#forward_to_tag_toggle (Some Tags.Script.sentence_end) in + (if stop#has_tag Tags.Script.sentence_end then ignore ( + stop#nocopy#forward_to_tag_toggle (Some Tags.Script.sentence_end))); + start,stop + +let end_tag_present end_iter = + end_iter#backward_char#has_tag Tags.Script.sentence_end + +let tag_on_insert = + let skip_last = ref (ref true) in (* ref to the mutable flag created on last call *) + fun buffer -> + let start,stop = get_sentence_bounds (buffer#get_iter_at_mark `INSERT) in + let skip_curr = ref true in (* shall the callback be skipped ? by default yes*) + let on_tag_fail buffer start _ = + skip_curr := false; (* tagging failed, we go to rescue mode *) + ignore (Glib.Timeout.add ~ms:1500 + ~callback:(fun () -> if not !skip_curr then begin + tag_slice buffer start buffer#end_iter (fun _ _ _ -> ()); + end; false)) + in + (!skip_last) := true; (* skip the previously created callback *) + skip_last := skip_curr; + tag_slice buffer start stop on_tag_fail + +let force_retag buffer = + tag_slice buffer buffer#start_iter buffer#end_iter (fun _ _ _ -> ()) + +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, + * don't move if into proof_decl and back_char not into proof_decl *) + if not (cursor#has_tag Tags.Script.proof_decl) then + ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl)); + if cursor#backward_char#has_tag Tags.Script.proof_decl then + ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl)); + let decl_start = cursor in + let prf_end = decl_start#forward_to_tag_toggle (Some Tags.Script.qed) in + let _,decl_end = get_sentence_bounds decl_start in + let _,prf_end = get_sentence_bounds prf_end in + if decl_start#has_tag Tags.Script.folded then ( + buffer#remove_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; + buffer#remove_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) + 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) class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs = object(self) @@ -590,7 +678,7 @@ object(self) input_buffer#set_modified false; pop_info (); flash_info "Buffer reverted"; - Highlight.highlight_all input_buffer; + force_retag input_buffer; with _ -> pop_info (); flash_info "Warning: could not revert buffer"; @@ -979,11 +1067,10 @@ object(self) None method find_phrase_starting_at (start:GText.iter) = - try - let end_iter = find_next_sentence start in + let _,end_iter = get_sentence_bounds start in + if end_tag_present end_iter then Some (start,end_iter) - with - | Not_found -> None + else None method complete_at_offset (offset:int) = prerr_endline ("Completion at offset : " ^ string_of_int offset); @@ -1413,42 +1500,6 @@ object(self) browse_keyword (self#insert_message) (get_current_word ()) - - - method toggle_proof_visibility (cursor:GText.iter) = - let start_keywords = ["Theorem";"Lemma";"Corollary";"Remark";"Proposition";"Fact";"Property"] in - (* let has_tag_by_name (it:GText.iter) name = - let tt = new GText.tag_table (input_buffer#tag_table) in - match tt#lookup name with - | Some named_tag -> it#has_tag (new GText.tag named_tag) - | _ -> false - in*) - try - let rec find_stmt_start from = - let cand_start = find_nearest_backward from start_keywords in - let cand_end = find_word_end cand_start in - let cand_word = input_buffer#get_text ~start:cand_start ~stop:cand_end () in - if List.mem cand_word start_keywords then cand_start else find_stmt_start cand_start - in - let stmt_start = find_stmt_start cursor in - let stmt_end = find_next_sentence stmt_start in - let proof_end = - find_next_sentence (find_nearest_forward stmt_end ["Qed";"Defined";"Admitted"]) - in - if stmt_start#has_tag Tags.Script.locked - then self#unhide_proof stmt_start stmt_end proof_end - else self#hide_proof stmt_start stmt_end proof_end - with - Not_found -> () - - method hide_proof (stmt_start:GText.iter) (stmt_end:GText.iter) (proof_end:GText.iter) = - input_buffer#apply_tag Tags.Script.hidden ~start:stmt_end ~stop:proof_end; - input_buffer#apply_tag Tags.Script.locked ~start:stmt_start ~stop:stmt_end - - method unhide_proof (stmt_start:GText.iter) (stmt_end:GText.iter) (proof_end:GText.iter) = - input_buffer#remove_tag Tags.Script.hidden ~start:stmt_end ~stop:proof_end; - input_buffer#remove_tag Tags.Script.locked ~start:stmt_start ~stop:stmt_end - initializer ignore (message_buffer#connect#insert_text ~callback:(fun it s -> ignore @@ -1508,7 +1559,7 @@ object(self) Tags.Script.error ~start:self#get_start_of_input ~stop; - Highlight.highlight_around_current_line + tag_on_insert input_buffer ) ); @@ -1586,23 +1637,6 @@ let create_session () = new analyzed_view script proof message stack in let _ = script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in - (* let _ = - List.map (fun (n,p) -> script#buffer#create_tag ~name:n p) - ["kwd",[`FOREGROUND "blue"]; - "decl",[`FOREGROUND "orange red"]; - "comment",[`FOREGROUND "brown"]; - "reserved",[`FOREGROUND "dark red"]; - "error",[`UNDERLINE `DOUBLE ; `FOREGROUND "red"]; - "to_process",[`BACKGROUND "light blue" ;`EDITABLE false]; - "processed",[`BACKGROUND "light green" ;`EDITABLE false]; - "unjustified",[`UNDERLINE `SINGLE; `FOREGROUND "red"; - `BACKGROUND "gold";`EDITABLE false]; - "found",[`BACKGROUND "blue"; `FOREGROUND "white"]; - "hidden",[`INVISIBLE true; `EDITABLE false]; - "locked",[`EDITABLE false; `BACKGROUND "light grey"] - ] in - let _ = - message#buffer#create_tag ~name:"error" [`FOREGROUND "red"] in*) let _ = proof#buffer#create_mark ~name:"end_of_conclusion" proof#buffer#start_iter in let _ = @@ -1876,7 +1910,6 @@ let main files = prerr_endline ("Loading: switch to view "^ string_of_int index); session_notebook#goto_page index; prerr_endline "Loading: highlight"; - Highlight.highlight_all input_buffer; input_buffer#set_modified false; prerr_endline "Loading: clear undo"; session.script#clear_undo; @@ -2074,7 +2107,7 @@ let main files = let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in ignore (rehighlight_m#connect#activate (fun () -> - Highlight.highlight_all + force_retag session_notebook#current_term.script#buffer; session_notebook#current_term.analyzed_view#recenter_insert)); @@ -2548,8 +2581,9 @@ let main files = ~tooltip:"Hide proof" ~key:GdkKeysyms._h ~callback:(fun x -> - let cav = session_notebook#current_term.analyzed_view in - cav#toggle_proof_visibility cav#get_insert) + let sess = session_notebook#current_term in + toggle_proof_visibility sess.script#buffer + sess.analyzed_view#get_insert) `MISSING_IMAGE; (* Tactics Menu *) diff --git a/ide/ide.mllib b/ide/ide.mllib index 73c1d0735..a235039b9 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -13,9 +13,9 @@ Config_lexer Utf8_convert Preferences Ideutils +CoqLex Gtk_parsing Undo -Highlight Coq Coq_commands Coq_tactics diff --git a/ide/syntaxBlocks.mll b/ide/syntaxBlocks.mll deleted file mode 100644 index 415ef6359..000000000 --- a/ide/syntaxBlocks.mll +++ /dev/null @@ -1,60 +0,0 @@ -(************************************************************************) -(* 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/tags.ml b/ide/tags.ml index 826fcd962..beb24071f 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -20,7 +20,9 @@ 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 error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"] @@ -29,8 +31,9 @@ struct 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 locked = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"] + let folded = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"] let paren = make_tag table ~name:"paren" [`BACKGROUND "purple"] + let sentence_end = make_tag table ~name:"sentence_end" [] end module Proof = struct |