From b45474e03dbba3687db4c7452432e686c32f60a4 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@cs.harvard.edu>
Date: Fri, 1 Aug 2014 21:22:11 -0400
Subject: Support for Timeout n and From ..

- The state machine gets kind of complex
  maybe it should become a parser at some point?
---
 tools/coqdep_lexer.mll | 46 ++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 42 insertions(+), 4 deletions(-)

(limited to 'tools/coqdep_lexer.mll')

diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 7d2978b25..4cb5e0087 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -49,6 +49,8 @@
 
   let syntax_error lexbuf =
     raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf))
+
+  let from_pre_ident = ref None
 }
 
 let space = [' ' '\t' '\n' '\r']
@@ -81,17 +83,21 @@ rule coq_action = parse
   | "Require" space+
       { require_file lexbuf }
   | "Require" space+ "Export" space+
-      { require_file lexbuf}
+      { require_file lexbuf }
   | "Require" space+ "Import" space+
-      { require_file lexbuf}
+      { require_file lexbuf }
   | "Local"? "Declare" space+ "ML" space+ "Module" space+
-      { mllist := []; modules lexbuf}
+      { mllist := []; modules lexbuf }
   | "Load" space+
       { load_file lexbuf }
   | "Add" space+ "LoadPath" space+
       { add_loadpath lexbuf }
   | "Time" space+
       { coq_action lexbuf }
+  | "Timeout" space+ ['0'-'9']+ space+
+      { coq_action lexbuf }
+  | "From" space+
+      { from_rule lexbuf }
   | space+
       { coq_action lexbuf }
   | "(*"
@@ -101,6 +107,33 @@ rule coq_action = parse
   | _
       { skip_to_dot lexbuf; coq_action lexbuf }
 
+and from_rule = parse
+  | "(*"
+      { comment_depth := 1; comment lexbuf; require_file lexbuf }
+  | space+
+      { from_rule lexbuf }
+  | coq_ident
+      { module_current_name := [Lexing.lexeme lexbuf];
+	from_pre_ident := Some (coq_qual_id_tail lexbuf);
+	module_names := [];
+	consume_require lexbuf }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { syntax_error lexbuf }
+
+and consume_require = parse
+  | "(*"
+      { comment_depth := 1; comment lexbuf; consume_require lexbuf }
+  | space+
+      { consume_require lexbuf }
+  | "Require" space+
+      { require_file lexbuf }
+  | eof
+      { syntax_error lexbuf }
+  | _
+      { syntax_error lexbuf }
+
 and add_loadpath = parse
   | "(*"
       { comment_depth := 1; comment lexbuf; add_loadpath lexbuf }
@@ -228,7 +261,12 @@ and require_file = parse
         module_names := [coq_qual_id_tail lexbuf];
         let qid = coq_qual_id_list lexbuf in
         parse_dot lexbuf;
-        Require qid }
+	match !from_pre_ident with
+	  None ->
+          Require qid
+	| Some from ->
+	  (from_pre_ident := None ;
+	   Require (List.map (fun x -> from @ x) qid)) }
   | '"' [^'"']* '"' (*'"'*)
       { let s = Lexing.lexeme lexbuf in
         parse_dot lexbuf;
-- 
cgit v1.2.3