summaryrefslogtreecommitdiff
path: root/ide/config_lexer.mll
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /ide/config_lexer.mll
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'ide/config_lexer.mll')
-rw-r--r--ide/config_lexer.mll10
1 files changed, 5 insertions, 5 deletions
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 7722e99a..97aeb2f5 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: config_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id$ *)
{
@@ -28,19 +28,19 @@ rule token = parse
| '#' [^ '\n']* { token lexbuf }
| ident { IDENT (lexeme lexbuf) }
| '=' { EQUAL }
- | '"' { Buffer.reset string_buffer;
+ | '"' { Buffer.reset string_buffer;
Buffer.add_char string_buffer '"';
string lexbuf;
let s = Buffer.contents string_buffer in
STRING (Scanf.sscanf s "%S" (fun s -> s)) }
| _ { let c = lexeme_start lexbuf in
- eprintf ".coqiderc: invalid character (%d)\n@." c;
+ eprintf ".coqiderc: invalid character (%d)\n@." c;
token lexbuf }
| eof { EOF }
and string = parse
| '"' { Buffer.add_char string_buffer '"' }
- | '\\' '"' | _
+ | '\\' '"' | _
{ Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf }
| eof { eprintf ".coqiderc: unterminated string\n@." }
@@ -60,7 +60,7 @@ and string = parse
| [] -> ()
| s :: sl -> fprintf fmt "%S@ %a" s print_list sl
in
- Stringmap.iter
+ Stringmap.iter
(fun k s -> fprintf fmt "@[<hov 2>%s = %a@]@\n" k print_list s) m;
fprintf fmt "@.";
close_out c