diff options
Diffstat (limited to 'ide/find_phrase.mll')
-rw-r--r-- | ide/find_phrase.mll | 74 |
1 files changed, 0 insertions, 74 deletions
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll deleted file mode 100644 index 23019185..00000000 --- a/ide/find_phrase.mll +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: find_phrase.mll 9240 2006-10-13 17:51:11Z notin $ *) - -{ - exception Lex_error of string - let length = ref 0 - let buff = Buffer.create 513 - -} - -let phrase_sep = '.' - -rule next_phrase = parse - | "(*" { incr length; incr length; - skip_comment lexbuf; - next_phrase lexbuf} - | '"'[^'"']*'"' { let lexeme = Lexing.lexeme lexbuf in - let ulen = Glib.Utf8.length lexeme in - length := !length + ulen; - Buffer.add_string buff lexeme; - next_phrase lexbuf - } - | phrase_sep[' ''\n''\t''\r'] { - begin - if !Preferences.current.Preferences.lax_syntax - then length := !length + 1 - else length := !length + 2 - end; - Buffer.add_string buff (Lexing.lexeme lexbuf); - Buffer.contents buff} - - | phrase_sep eof{ - length := !length + 1; - Buffer.add_string buff (Lexing.lexeme lexbuf); - Buffer.contents buff} - | phrase_sep phrase_sep - { - length := !length + 2; - Buffer.add_string buff (Lexing.lexeme lexbuf); - next_phrase lexbuf - } - | _ - { - let c = Lexing.lexeme_char lexbuf 0 in - if Ideutils.is_char_start c then incr length; - Buffer.add_char buff c ; - next_phrase lexbuf - } - | eof { raise (Lex_error "Phrase should end with . followed by a separator") } -and skip_comment = parse - | "*)" {incr length; incr length; ()} - | "(*" {incr length; incr length; - skip_comment lexbuf; - skip_comment lexbuf} - | _ { if Ideutils.is_char_start (Lexing.lexeme_char lexbuf 0) then - incr length; - skip_comment lexbuf} - | eof { raise (Lex_error "No closing *)") } - - -{ - let get lb = - Buffer.reset buff; - length := 0; - next_phrase lb - -} |