1 files changed, 66 insertions, 0 deletions
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
new file mode 100644
index 00000000..8081474f
--- /dev/null
+++ b/ide/find_phrase.mll
@@ -0,0 +1,66 @@
+(************************************************************************)
+(*  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,v 1.8.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+
+{
+  exception Lex_error of string
+  let length = ref 0
+  let buff = Buffer.create 513
+  exception EOF of string
+
+}
+
+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'] {
+      length := !length + 2; 
+      Buffer.add_string buff (Lexing.lexeme lexbuf);
+      Buffer.contents buff}
+
+  | phrase_sep eof{
+      length := !length + 2; 
+      Buffer.add_string buff (Lexing.lexeme lexbuf);
+      Buffer.add_char buff '\n';
+      raise (EOF(Buffer.contents buff))}
+  | _ 
+      { 
+	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
+
+}