Using an algebraic type for distinguishing toplevel input from location in file.

4 files changed, 24 insertions, 18 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 636027f9b4..9c9189ffeb 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -10,8 +10,19 @@ open Pp
 open Util
 open Tok
 
+(** Location utilities  *)
+let ploc_file_of_coq_file = function
+| Loc.ToplevelInput -> ""
+| Loc.InFile f -> f
+
+let coq_file_of_ploc_file s =
+  if s = "" then Loc.ToplevelInput else Loc.InFile s
+
+let from_coqloc fname line_nb bol_pos bp ep =
+  Ploc.make_loc (ploc_file_of_coq_file fname) line_nb bol_pos (bp, ep) ""
+
 let to_coqloc loc =
-  { Loc.fname = Ploc.file_name loc;
+  { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
     Loc.line_nb = Ploc.line_nb loc;
     Loc.bol_pos = Ploc.bol_pos loc;
     Loc.bp = Ploc.first_pos loc;
@@ -118,14 +129,6 @@ let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
 
-(** Location utilities  *)
-let file_loc_of_file = function
-| None -> ""
-| Some f -> f
-
-let make_loc fname line_nb bol_pos bp ep =
-  Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) ""
-
 (* Update a loc without allocating an intermediate pair *)
 let set_loc_pos loc bp ep =
   Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp)
@@ -369,7 +372,7 @@ let rec string loc ~comm_level bp len = parser
      err loc Unterminated_string
 
 (* To associate locations to a file name *)
-let current_file = ref None
+let current_file = ref Loc.ToplevelInput
 
 (* Utilities for comments in beautify *)
 let comment_begin = ref None
@@ -392,7 +395,7 @@ let rec split_comments comacc acc pos = function
 let extract_comments pos = split_comments [] [] pos !comments
 
 (* The state of the lexer visible from outside *)
-type lexer_state = int option * string * bool * ((int * int) * string) list * string option
+type lexer_state = int option * string * bool * ((int * int) * string) list * Loc.source
 
 let init_lexer_state f = (None,"",true,[],f)
 let set_lexer_state (o,s,b,c,f) =
@@ -404,7 +407,7 @@ let set_lexer_state (o,s,b,c,f) =
 let release_lexer_state () =
   (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file)
 let drop_lexer_state () =
-    set_lexer_state (init_lexer_state None)
+    set_lexer_state (init_lexer_state Loc.ToplevelInput)
 
 let real_push_char c = Buffer.add_char current_comment c
 
@@ -672,7 +675,7 @@ let token_text = function
 
 let func cs =
   let loct = loct_create () in
-  let cur_loc = ref (make_loc !current_file 1 0 0 0) in
+  let cur_loc = ref (from_coqloc !current_file 1 0 0 0) in
   let ts =
     Stream.from
       (fun i ->
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 77d652b185..d3ef19873f 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -49,7 +49,7 @@ end
 (* Mainly for comments state, etc... *)
 type lexer_state
 
-val init_lexer_state : string option -> lexer_state
+val init_lexer_state : Loc.source -> lexer_state
 val set_lexer_state : lexer_state -> unit
 val release_lexer_state : unit -> lexer_state
 val drop_lexer_state : unit -> unit
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 81f02bf955..0a4411233e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -15,8 +15,11 @@ let curry f x y = f (x, y)
 let uncurry f (x,y) = f x y
 
 (** Location Utils  *)
+let coq_file_of_ploc_file s =
+  if s = "" then Loc.ToplevelInput else Loc.InFile s
+
 let to_coqloc loc =
-  { Loc.fname = Ploc.file_name loc;
+  { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
     Loc.line_nb = Ploc.line_nb loc;
     Loc.bol_pos = Ploc.bol_pos loc;
     Loc.bp = Ploc.first_pos loc;
@@ -80,7 +83,7 @@ module type S =
       Gramext.position option * single_extend_statment list
   type coq_parsable
 
-  val parsable : ?file:string -> char Stream.t -> coq_parsable
+  val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
@@ -104,7 +107,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
       Gramext.position option * single_extend_statment list
   type coq_parsable = parsable * CLexer.lexer_state ref
 
-  let parsable ?file c =
+  let parsable ?(file=Loc.ToplevelInput) c =
     let state = ref (CLexer.init_lexer_state file) in
     CLexer.set_lexer_state !state;
     let a = parsable c in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 445818e130..ecb0ddd4f3 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -73,7 +73,7 @@ module type S =
 
   type coq_parsable
 
-  val parsable : ?file:string -> char Stream.t -> coq_parsable
+  val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a