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

11 files changed, 51 insertions, 29 deletions

diff --git a/API/API.mli b/API/API.mli
index 8b0bef48c..a3701621e 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4703,7 +4703,7 @@ sig
 
     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
diff --git a/lib/loc.ml b/lib/loc.ml
index 9f036d90f..06da13d44 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -8,8 +8,12 @@
 
 (* Locations management *)
 
+type source =
+  | InFile of string
+  | ToplevelInput
+
 type t = {
-  fname : string; (** filename *)
+  fname : source; (** filename or toplevel input *)
   line_nb : int; (** start line number *)
   bol_pos : int; (** position of the beginning of start line *)
   line_nb_last : int; (** end line number *)
@@ -23,10 +27,15 @@ let create fname line_nb bol_pos bp ep = {
   line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; }
 
 let make_loc (bp, ep) = {
-  fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+  fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
   bp = bp; ep = ep; }
 
+let mergeable loc1 loc2 =
+  loc1.fname = loc2.fname
+
 let merge loc1 loc2 =
+  if not (mergeable loc1 loc2) then
+    failwith "Trying to merge unmergeable locations.";
   if loc1.bp < loc2.bp then
     if loc1.ep < loc2.ep then {
       fname = loc1.fname;
diff --git a/lib/loc.mli b/lib/loc.mli
index 1fbaae836..d4061e044 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -8,8 +8,12 @@
 
 (** {5 Basic types} *)
 
+type source =
+  | InFile of string
+  | ToplevelInput
+
 type t = {
-  fname : string; (** filename *)
+  fname : source; (** filename or toplevel input *)
   line_nb : int; (** start line number *)
   bol_pos : int; (** position of the beginning of start line *)
   line_nb_last : int; (** end line number *)
@@ -22,7 +26,7 @@ type t = {
 
 (** This is inherited from CAMPL4/5. *)
 
-val create : string -> int -> int -> int -> int -> t
+val create : source -> int -> int -> int -> int -> t
 (** Create a location from a filename, a line number, a position of the
     beginning of the line, a start and end position *)
 
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 636027f9b..9c9189ffe 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 77d652b18..d3ef19873 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 81f02bf95..0a4411233 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 445818e13..ecb0ddd4f 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
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index d76703d98..444bf8a8f 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -155,14 +155,16 @@ let error_info_for_buffer ?loc buf =
       let fname = loc.Loc.fname in
       let hl, loc =
         (* We are in the toplevel *)
-        if CString.equal fname "" then
+        match fname with
+        | Loc.ToplevelInput ->
           let nloc = adjust_loc_buf buf loc in
           if valid_buffer_loc buf loc then
             (fnl () ++ print_highlight_location buf nloc, nloc)
             (* in the toplevel, but not a valid buffer *)
           else (mt (), nloc)
           (* we are in batch mode, don't adjust location *)
-        else (mt (), loc)
+        | Loc.InFile _ ->
+           (mt (), loc)
       in Topfmt.pr_loc loc ++ hl
     ) loc
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bfab44770..1602f9c68 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -182,7 +182,7 @@ and load_vernac verbosely sid file =
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in
   let in_chan = open_utf8_file_in file in
   let in_echo = if verbosely then Some (open_utf8_file_in file) else None in
-  let in_pa   = Pcoq.Gram.parsable ~file (Stream.of_channel in_chan) in
+  let in_pa   = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
   let rsid = ref sid in
   try
     (* we go out of the following infinite loop when a End_of_input is
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index e7b14309d..6a10eb43a 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -292,10 +292,11 @@ let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
 (* This is specific to the toplevel *)
 let pr_loc loc =
     let fname = loc.Loc.fname in
-    if CString.equal fname "" then
+    match fname with
+    | Loc.ToplevelInput ->
       Loc.(str"Toplevel input, characters " ++ int loc.bp ++
 	   str"-" ++ int loc.ep ++ str":")
-    else
+    | Loc.InFile fname ->
       Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
 	   str", line " ++ int loc.line_nb ++ str", characters " ++
 	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d2ba9eb1c..22306ac5b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1902,7 +1902,7 @@ let vernac_load interp fname =
   let input =
     let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
-    Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in
+    Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
   try while true do interp (snd (parse_sentence input)) done
   with End_of_input -> ()