Generalized the possibility to refer to a global name by a notation

string in most commands expecting a global name (e.g. 'Print "+"' for
an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation,
possibly surrounded by a scope delimiter). Support for such smart
globals in VERNAC EXTEND to do.

Added a file smartlocate.ml for high-level globalization functions.

Mini-nettoyage metasyntax.ml.



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

1 files changed, 26 insertions, 38 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index adf3e93a4..54cbc0ae3 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -240,8 +240,6 @@ let parse_format (loc,str) =
 
 type symbol_token = WhiteSpace of int | String of string
 
-(* Decompose the notation string into tokens *)
-
 let split_notation_string str =
   let push_token beg i l =
     if beg = i then l else
@@ -307,10 +305,6 @@ let rec interp_list_parser hd = function
 
 (* Find non-terminal tokens of notation *)
 
-let unquote_notation_token s =
-  let n = String.length s in
-  if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
-
 let is_normal_token str =
   try let _ = Lexer.check_ident str in true with Lexer.Error _ -> false
 
@@ -321,26 +315,18 @@ let quote_notation_token x =
   if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
   else x
 
-let rec raw_analyse_notation_tokens = function
-  | []    -> [], []
-  | String ".." :: sl ->
-      let (vars,l) = raw_analyse_notation_tokens sl in
-      (list_add_set ldots_var vars, NonTerminal ldots_var :: l)
+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_normal_token x ->
       Lexer.check_ident x;
-      let id = Names.id_of_string x in
-      let (vars,l) = raw_analyse_notation_tokens sl in
-      if List.mem id vars then
-	error ("Variable "^x^" occurs more than once.");
-      (id::vars, NonTerminal id :: l)
+      NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl
   | String s :: sl ->
       Lexer.check_keyword s;
-      let (vars,l) = raw_analyse_notation_tokens sl in
-      (vars, Terminal (unquote_notation_token s) :: l)
+      Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl
   | WhiteSpace n :: sl ->
-      let (vars,l) = raw_analyse_notation_tokens sl in
-      (vars, Break n :: l)
+      Break n :: raw_analyze_notation_tokens sl
 
 let is_numeral symbs = 
   match List.filter (function Break _ -> false | _ -> true) symbs with
@@ -349,8 +335,23 @@ let is_numeral symbs =
   | _ ->
       false
 
-let analyse_notation_tokens l =
-  let vars,l = raw_analyse_notation_tokens l in
+let rec get_notation_vars = function
+  | [] -> []
+  | NonTerminal id :: sl ->
+      let vars = get_notation_vars sl in
+      if List.mem id vars then
+        if id <> ldots_var then
+	  error ("Variable "^string_of_id id^" occurs more than once.")
+        else
+          vars
+      else
+        id::vars
+  | (Terminal _ | Break _) :: sl -> get_notation_vars sl
+  | SProdList _ :: _ -> assert false
+
+let analyze_notation_tokens l =
+  let l = raw_analyze_notation_tokens l in
+  let vars = get_notation_vars l in
   let extrarecvars,recvars,l = interp_list_parser [] l in
   (if extrarecvars = [] then [], [], vars, l
    else extrarecvars, recvars, list_subtract vars recvars, l)
@@ -538,7 +539,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
       when s' = String.make (String.length s') ' ' ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
   | Terminal s :: symbs, (UnpTerminal s') :: fmt
-      when s = unquote_notation_token s' ->
+      when s = drop_simple_quotes s' ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
       let i = list_index s vars in
@@ -829,7 +830,7 @@ let compute_syntax_data (df,modifiers) =
   (* Notation defaults to NONA *)
   let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
   let toks = split_notation_string df in
-  let (extrarecvars,recvars,vars,symbols) = analyse_notation_tokens toks in
+  let (extrarecvars,recvars,vars,symbols) = analyze_notation_tokens toks in
   let ntn_for_interp = make_notation_key symbols in
   let symbols' = remove_curly_brackets symbols in
   let need_squash = (symbols <> symbols') in
@@ -962,7 +963,7 @@ let add_notation_in_scope local df c mods scope =
 
 let add_notation_interpretation_core local df names c scope onlyparse =
   let dfs = split_notation_string df in
-  let (extrarecvars,recvars,vars,symbs) = analyse_notation_tokens dfs in
+  let (extrarecvars,recvars,vars,symbs) = analyze_notation_tokens dfs in
   (* Redeclare pa/pp rules *)
   if not (is_numeral symbs) then begin
     let sy_rules = recover_notation_syntax (make_notation_key symbs) in
@@ -1016,19 +1017,6 @@ let add_infix local (inf,modifiers) pr sc =
   add_notation local c (df,modifiers) sc
 
 (**********************************************************************)
-(* Miscellaneous                                                      *)
-
-let standardize_locatable_notation ntn =
-  let unquote = function
-    | String s -> [unquote_notation_token s]
-    | _ -> [] in
-  if String.contains ntn ' ' then
-    String.concat " " 
-      (List.flatten (List.map unquote (split_notation_string ntn)))
-  else
-    unquote_notation_token ntn
-
-(**********************************************************************)
 (* Delimiters and classes bound to scopes                             *)
 
 type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ