aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/coq.ml26
-rw-r--r--ide/coqide.ml9
-rw-r--r--ide/gtk_parsing.ml8
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