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/gtk_parsing.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/gtk_parsing.ml')
-rw-r--r-- | ide/gtk_parsing.ml | 8 |
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 |