From 7e71f5071b19415b4b285702e1753c9a82523acb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 19 Dec 2014 14:47:01 +0100
Subject: Use Unix.create_process instead of Sys.command to run external tools.
 Revised parsing of compcert.ini file to split arguments into words like POSIX
 shell does (including quotes).

---
 lib/Readconfig.mll | 111 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 111 insertions(+)
 create mode 100644 lib/Readconfig.mll

(limited to 'lib/Readconfig.mll')

diff --git a/lib/Readconfig.mll b/lib/Readconfig.mll
new file mode 100644
index 00000000..27ef32cf
--- /dev/null
+++ b/lib/Readconfig.mll
@@ -0,0 +1,111 @@
+{
+
+(* Recording key=val bindings *)
+
+let key_val_tbl : (string, string list) Hashtbl.t = Hashtbl.create 17
+
+let key_val key =
+  try Some(Hashtbl.find key_val_tbl key) with Not_found -> None
+
+(* Auxiliaries for parsing *)
+
+let buf = Buffer.create 32
+
+let stash inword words =
+  if inword then begin
+    let w = Buffer.contents buf in
+    Buffer.clear buf;
+    w :: words
+  end else
+    words
+
+(* Error reporting *)
+
+exception Error of string * int * string
+
+let error msg lexbuf =
+  Lexing.(raise (Error(lexbuf.lex_curr_p.pos_fname,
+                       lexbuf.lex_curr_p.pos_lnum,
+                       msg)))
+
+let ill_formed_line lexbuf = error "Ill-formed line" lexbuf 
+let unterminated_quote lexbuf = error "Unterminated quote" lexbuf
+let lone_backslash lexbuf = error "Lone \\ (backslash) at end of file" lexbuf
+
+}
+
+let whitespace = [' ' '\t' '\012' '\r']
+let newline = '\r'* '\n'
+let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']*
+
+rule begline = parse
+  | '#' [^ '\n']* ('\n' | eof)
+      { Lexing.new_line lexbuf; begline lexbuf }
+  | whitespace* (ident as key) whitespace* '=' 
+      { let words = unquoted false [] lexbuf in
+        Hashtbl.add key_val_tbl key (List.rev words);
+        begline lexbuf }
+  | eof
+      { () }
+  | _
+      { ill_formed_line lexbuf }
+
+and unquoted inword words = parse
+  | '\n' | eof    { Lexing.new_line lexbuf; stash inword words }
+  | whitespace+   { unquoted false (stash inword words) lexbuf }
+  | '\\' newline  { Lexing.new_line lexbuf; unquoted inword words lexbuf }
+  | '\\' (_ as c) { Buffer.add_char buf c; unquoted true words lexbuf }
+  | '\\' eof      { lone_backslash lexbuf }
+  | '\''          { singlequote lexbuf; unquoted true words lexbuf }
+  | '\"'          { doublequote lexbuf; unquoted true words lexbuf }
+  | _ as c        { Buffer.add_char buf c; unquoted true words lexbuf }
+
+and singlequote = parse
+  | eof           { unterminated_quote lexbuf }
+  | '\''          { () }
+  | newline       { Lexing.new_line lexbuf;
+                    Buffer.add_char buf '\n'; singlequote lexbuf }
+  | _ as c        { Buffer.add_char buf c; singlequote lexbuf }
+
+and doublequote = parse
+  | eof           { unterminated_quote lexbuf }
+  | '\"'          { () }
+  | '\\' newline  { Lexing.new_line lexbuf; doublequote lexbuf }
+  | '\\' (['$' '`' '\"' '\\'] as c)
+                  { Buffer.add_char buf c; doublequote lexbuf }
+  | newline       { Lexing.new_line lexbuf;
+                    Buffer.add_char buf '\n'; doublequote lexbuf }
+  | _ as c        { Buffer.add_char buf c; doublequote lexbuf }
+
+{
+
+(* The entry point *)
+
+let read_config_file filename =
+  let ic = open_in filename in
+  let lexbuf = Lexing.from_channel ic in
+  Lexing.(lexbuf.lex_start_p <- {lexbuf.lex_start_p with pos_fname = filename});
+  try
+    Hashtbl.clear key_val_tbl;
+    begline lexbuf;
+    close_in ic
+  with x ->
+    close_in ic; raise x
+
+(* Test harness *)
+(*
+open Printf
+
+let _ =
+  Hashtbl.clear key_val_tbl;
+  begline (Lexing.from_channel stdin);
+  Hashtbl.iter
+    (fun key value ->
+      printf "%s =" key;
+      List.iter (fun v -> printf " |%s|" v) value;
+      printf "\n")
+    key_val_tbl
+*)
+
+}
+
-- 
cgit