diff options
author | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-05-13 07:31:28 +0000 |
---|---|---|
committer | vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-05-13 07:31:28 +0000 |
commit | f101dec29d5ec92c2eaeaac0af8dd43a2fd1112e (patch) | |
tree | a49bd34eeecc129cf998ccd9694c7a3e4b4767bd /ide/coqide.ml | |
parent | 28a38529e47d2593a7af41a7223208e2dd049179 (diff) |
minor bugfixes. CoqIde development will resume soon now ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12124 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r-- | ide/coqide.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 449f84bcc..6fd533334 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1434,6 +1434,7 @@ object(self) 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 @@ -1441,9 +1442,13 @@ object(self) | _ -> false in try - let stmt_start = - find_nearest_backward cursor ["Theorem";"Lemma";"Corollary";"Remark";"Proposition";"Fact";"Property"] + 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"]) |