diff options
| -rw-r--r-- | ide/coq.ml | 26 | ||||
| -rw-r--r-- | ide/coqide.ml | 9 | ||||
| -rw-r--r-- | ide/gtk_parsing.ml | 8 |
3 files changed, 14 insertions, 29 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index fc10dacfd..505140cf2 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -425,8 +425,9 @@ let interp_with_options verbosely options s = prerr_endline s; let pa = Pcoq.Gram.parsable (Stream.of_string s) in let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in - (* Temporary hack to make coqide.byte work (WTF???) *) - Pervasives.prerr_endline ""; + (* Temporary hack to make coqide.byte work (WTF???) - now with less screen + * pollution *) + Pervasives.prerr_string " \r"; Pervasives.flush stderr; match pe with | None -> assert false | Some((loc,vernac) as last) -> @@ -702,24 +703,3 @@ let current_status () = path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ())) with _ -> path - - -(* analyzed_view's methods that use stuff here - * - * process_next_phrase - * undo_last_step - * go_to_insert - * reset_initial - * process_until_end_or_error - * show_goals - *) - -(* process_next_phrase => - * - * send_to_coq - * * interp_and_replace | interp - * push_phrase - * get_current_goals - *) - -(* functions called by analyzed_view's method *) 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"]) diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index be5bb84e9..8da4d9dda 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -122,14 +122,14 @@ let find_comment_end (start:GText.iter) = let rec find_string_end (start:GText.iter) = - let backslash = int_of_char '\\' in - let rec escape c = - (c#char = backslash) && not (escape c#backward_char) + let dblquote = int_of_char '"' in + let rec escaped_dblquote c = + (c#char = dblquote) && not (escaped_dblquote c#backward_char) in match start#forward_search "\"" with | None -> raise Not_found | Some (stop,next_start) -> - if escape stop#backward_char + if escaped_dblquote stop#backward_char then find_string_end next_start else next_start |