Mise en place de parseurs avec globalisation pas seulement dans les quotations, pour utilisation par les règles de syntaxe et grammaire

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

4 files changed, 36 insertions, 4 deletions

diff --git a/parsing/extend.ml4 b/parsing/extend.ml4
index 1e2a00ccec..515cdd9790 100644
--- a/parsing/extend.ml4
+++ b/parsing/extend.ml4
@@ -8,6 +8,23 @@ open Pcoq
 open Coqast
 open Ast
 
+(* Done here to get parsing/g_*.ml4 non dependent from kernel *)
+let constr_parser_with_glob = map_entry Astterm.globalize_ast Constr.constr
+let tactic_parser_with_glob = map_entry Astterm.globalize_ast Tactic.tactic
+let vernac_parser_with_glob = map_entry Astterm.globalize_ast Vernac.vernac
+
+(* This updates default parsers for Grammar actions and Syntax *)
+(* patterns by inserting globalization *)
+let _ = update_constr_parser constr_parser_with_glob
+let _ = update_tactic_parser tactic_parser_with_glob
+let _ = update_vernac_parser vernac_parser_with_glob
+
+(* This installs default quotations parsers to escape the ast parser *)
+(* "constr" is used by default in quotations found in the ast parser *) 
+let _ = define_quotation true "constr" constr_parser_with_glob
+let _ = define_quotation false "tactic" tactic_parser_with_glob
+let _ = define_quotation false "vernac" vernac_parser_with_glob
+
 (* Converting and checking grammar command *)
 
 type nonterm =
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 8128cb3d99..26f946d031 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -9,7 +9,7 @@ open Names
 open Ast
 
 let get_z_sign loc =
-  let ast_of_id id = Astterm.globalize_command (Nvar(loc,id)) in
+  let ast_of_id id = Astterm.globalize_constr (Nvar(loc,id)) in
   ((ast_of_id "xI", ast_of_id "xO", ast_of_id "xH"),
    (ast_of_id "ZERO", ast_of_id "POS", ast_of_id "NEG"),
    (ast_of_id "My_special_variable0", ast_of_id "My_special_variable1"))
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index fbb00511c8..01ae437a87 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -425,6 +425,18 @@ let define_quotation default s e =
 
 let _ = define_quotation false "ast" ast in ()
 
+let constr_parser = ref Constr.constr
+let tactic_parser = ref Tactic.tactic
+let vernac_parser = ref Vernac.vernac
+
+let update_constr_parser p = constr_parser := p
+let update_tactic_parser p = tactic_parser := p
+let update_vernac_parser p = vernac_parser := p
+
+(**********************************************************************)
+(* The following is to dynamically set the parser in Grammar actions  *)
+(* and Syntax pattern, according to the universe of the rule defined  *)
+
 let default_action_parser_ref = ref ast
 
 let get_default_action_parser () = !default_action_parser_ref
@@ -432,9 +444,9 @@ let get_default_action_parser () = !default_action_parser_ref
 let set_default_action_parser f = (default_action_parser_ref := f)
 
 let set_default_action_parser_by_name = function
-  | "constr" -> set_default_action_parser Constr.constr
-  | "tactic" -> set_default_action_parser Tactic.tactic
-  | "vernac" -> set_default_action_parser Vernac.vernac
+  | "constr" -> set_default_action_parser constr_parser
+  | "tactic" -> set_default_action_parser tactic_parser
+  | "vernac" -> set_default_action_parser vernac_parser
   | _ -> set_default_action_parser ast
 
 let default_action_parser =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d687bb9d33..d2bb4b947e 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -51,6 +51,9 @@ val force_entry_type : string * gram_universe -> string ->
 (* Quotations *)
 
 val define_quotation : bool -> string -> (Coqast.t Gram.Entry.e) -> unit
+val update_constr_parser : Coqast.t Gram.Entry.e -> unit
+val update_tactic_parser : Coqast.t Gram.Entry.e -> unit
+val update_vernac_parser : Coqast.t Gram.Entry.e -> unit
 
 (* The default parser for actions in grammar rules *)