Moved Compat to parsing. This permits to break the dependency of the

kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.

This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 27 insertions, 9 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index d1e379cca2..c6e694902a 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -44,6 +44,11 @@ let explain_exn_default = function
       hov 0 ((if loc = Loc.ghost then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
                ++ Errors.print_no_anomaly exc)
+  | Compat.Exc_located (loc, exc) ->
+      let loc = Compat.to_coqloc loc in
+      hov 0 ((if loc = Loc.ghost then (mt ())
+               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
+               ++ Errors.print_no_anomaly exc)
   | EvaluatedError (msg,None) -> msg
   | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise
   (* Otherwise, not handled here *)
@@ -110,6 +115,9 @@ let rec process_vernac_interp_error = function
         Some (process_vernac_interp_error exc))
   | Loc.Exc_located (loc,exc) ->
       Loc.Exc_located (loc,process_vernac_interp_error exc)
+  | Compat.Exc_located (loc, exc) ->
+      let loc = Compat.to_coqloc loc in
+      Loc.Exc_located (loc, process_vernac_interp_error exc)
   | exc ->
       exc
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 8bfcfea6ae..bd426b6fd3 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -292,8 +292,13 @@ let eval_call c =
       | Errors.Quit -> None, "Quit is not allowed by coqide!"
       | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
       | Error_in_file (_,_,inner) -> None, pr_exn inner
-      | Loc.Exc_located (loc, inner) when loc = Loc.ghost -> None, pr_exn inner
-      | Loc.Exc_located (loc, inner) -> Some (Loc.unloc loc), pr_exn inner
+      | Loc.Exc_located (loc, inner) ->
+        let loc = if loc = Loc.ghost then None else Some (Loc.unloc loc) in
+        loc, pr_exn inner
+      | Compat.Exc_located (loc, inner) ->
+        let loc = Compat.to_coqloc loc in
+        let loc = if loc = Loc.ghost then None else Some (Loc.unloc loc) in
+        loc, pr_exn inner
       | e -> None, pr_exn e
   in
   let interruptible f x =
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a665dc3736..d406bf8d91 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -24,7 +24,6 @@ open Vernacexpr
 open Pcoq
 open Libnames
 open Tok
-open Lexer
 open Egramml
 open Egramcoq
 open Notation
@@ -33,7 +32,7 @@ open Nameops
 (**********************************************************************)
 (* Tokens                                                             *)
 
-let cache_token (_,s) = add_keyword s
+let cache_token (_,s) = Lexer.add_keyword s
 
 let inToken : string -> obj =
   declare_object {(default_object "TOKEN") with
@@ -159,7 +158,7 @@ let pr_grammar = function
 (* Parse a format (every terminal starting with a letter or a single
    quote (except a single quote alone) must be quoted) *)
 
-let parse_format (loc,str) =
+let parse_format ((loc, str) : lstring) =
   let str = " "^str in
   let l = String.length str in
   let push_token a = function
@@ -334,7 +333,7 @@ let rec interp_list_parser hd = function
 (* To protect alphabetic tokens and quotes from being seen as variables *)
 let quote_notation_token x =
   let n = String.length x in
-  let norm = is_ident x in
+  let norm = Lexer.is_ident x in
   if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
   else x
 
@@ -342,7 +341,7 @@ let rec raw_analyze_notation_tokens = function
   | []    -> []
   | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
   | String "_" :: _ -> error "_ must be quoted."
-  | String x :: sl when is_ident x ->
+  | String x :: sl when Lexer.is_ident x ->
       NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl
   | String s :: sl ->
       Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl
@@ -643,12 +642,12 @@ let make_production etyps symbols =
 	    let typ = List.assoc m etyps in
 	    distribute [GramConstrNonTerminal (typ, Some m)] ll
         | Terminal s ->
-	    distribute [GramConstrTerminal (terminal s)] ll
+	    distribute [GramConstrTerminal (Lexer.terminal s)] ll
         | Break _ ->
             ll
         | SProdList (x,sl) ->
             let tkl = List.flatten
-              (List.map (function Terminal s -> [terminal s]
+              (List.map (function Terminal s -> [Lexer.terminal s]
                 | Break _ -> []
                 | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in
 	    match List.assoc x etyps with
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 74ed231d17..7e301ba0e6 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -291,6 +291,12 @@ let print_toplevel_error exc =
             (print_highlight_location top_buffer loc, ie)
           else
 	    ((mt ()) (* print_command_location top_buffer dloc *), ie)
+      | Compat.Exc_located (loc, ie) ->
+          let loc = Compat.to_coqloc loc in
+          if valid_buffer_loc top_buffer dloc loc then
+            (print_highlight_location top_buffer loc, ie)
+          else
+            ((mt ()) (* print_command_location top_buffer dloc *), ie)
       | Error_in_file (s, (inlibrary, fname, loc), ie) ->
           (print_location_in_file s inlibrary fname loc, ie)
       | _ ->