From e44e2381045d8d373df9cb47855fc5b36f38d7d1 Mon Sep 17 00:00:00 2001 From: vgross Date: Fri, 13 Nov 2009 13:36:13 +0000 Subject: new handling for lexical structures. Sentence extraction and proof folding is now done with tags. The lexer has been modified to use a callback to "stamp" the lexical constructs that must be distinguished. new funcs in ide/coqide.ml : apply_tag : GText.buffer -> GText.iter -> (int -> int) -> int -> int -> CoqLex.token -> unit remove_tags : GText.buffer -> GText.iter -> GText.iter -> unit tag_slice : GText.buffer -> GText.iter -> GText.iter -> (GText.buffer -> GText.iter -> GText.iter) -> unit get_sentence_bounds : GText.iter -> GText.iter * GText.iter end_tag_present : GText.iter -> bool tag_on_insert : GText.buffer -> unit force_retag : GText.buffer -> unit toggle_proof_visibility : GText.buffer -> GText.iter -> unit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12517 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqLex.mll | 194 +++++++++++++++++++++++++++++++++++++++++++++++++++ ide/coqide.ml | 168 ++++++++++++++++++++++++++------------------ ide/ide.mllib | 2 +- ide/syntaxBlocks.mll | 60 ---------------- ide/syntaxTokens.mll | 158 ----------------------------------------- ide/tags.ml | 5 +- 6 files changed, 300 insertions(+), 287 deletions(-) create mode 100644 ide/coqLex.mll delete mode 100644 ide/syntaxBlocks.mll delete mode 100644 ide/syntaxTokens.mll diff --git a/ide/coqLex.mll b/ide/coqLex.mll new file mode 100644 index 000000000..03ce950fd --- /dev/null +++ b/ide/coqLex.mll @@ -0,0 +1,194 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Hashtbl.add h s ()) + [ "Add" ; "Check"; "Eval"; "Extraction" ; + "Load" ; "Undo"; "Goal"; + "Proof" ; "Print";"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 ()) + [ (* 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 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 +| "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 } + | "\"" { Lexing.lexeme_end lexbuf } + | eof { Lexing.lexeme_end lexbuf } + | _ { coq_string lexbuf } + +and comment = parse + | "(*" { ignore (comment lexbuf); comment lexbuf } + | "\"" { ignore (coq_string lexbuf); comment lexbuf } + | "*)" { Lexing.lexeme_end lexbuf } + | eof { Lexing.lexeme_end lexbuf } + | _ { comment 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; + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration + end; + sentence stamp lexbuf + } + | multiword_command { + if !start then begin + start := false; + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword + end; + sentence stamp lexbuf } + | ident as id { + if !start then begin + start := false; + if id <> "Time" then begin + 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 + 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 + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword + end; + sentence stamp lexbuf } + | ".." + | _ { sentence stamp lexbuf} + | sentence_sep { } + | eof { raise Not_found } + +{ + let find_end_offset stamp slice = + let lb = Lexing.from_string slice in + start := true; + 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 *) -(* 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 -} 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 -- cgit v1.2.3