aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/gtk_parsing.ml
diff options
context:
space:
mode:
authorGravatar vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-05-13 07:31:28 +0000
committerGravatar vgross <vgross@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-05-13 07:31:28 +0000
commitf101dec29d5ec92c2eaeaac0af8dd43a2fd1112e (patch)
treea49bd34eeecc129cf998ccd9694c7a3e4b4767bd /ide/gtk_parsing.ml
parent28a38529e47d2593a7af41a7223208e2dd049179 (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/gtk_parsing.ml')
-rw-r--r--ide/gtk_parsing.ml8
1 files changed, 4 insertions, 4 deletions
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