From f101dec29d5ec92c2eaeaac0af8dd43a2fd1112e Mon Sep 17 00:00:00 2001
From: vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 13 May 2009 07:31:28 +0000
Subject: 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
---
 ide/coq.ml         | 26 +++-----------------------
 ide/coqide.ml      |  9 +++++++--
 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
 
-- 
cgit v1.2.3