More flexibility in locating or referring to a notation.

We generalize the possibility to refer to a notation not only by its
"_ U _" form but also using its "a 'U' b".

(Wish from EJGA)

1 files changed, 6 insertions, 51 deletions

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 1b9cfc07e..a1c8902c5 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -199,36 +199,6 @@ let parse_format ((loc, str) : lstring) =
 (***********************)
 (* Analyzing notations *)
 
-type symbol_token = WhiteSpace of int | String of string
-
-let split_notation_string str =
-  let push_token beg i l =
-    if Int.equal beg i then l else
-      let s = String.sub str beg (i - beg) in
-      String s :: l
-  in
-  let push_whitespace beg i l =
-    if Int.equal beg i then l else WhiteSpace (i-beg) :: l
-  in
-  let rec loop beg i =
-    if i < String.length str then
-      if str.[i] == ' ' then
-	push_token beg i (loop_on_whitespace (i+1) (i+1))
-      else
-	loop beg (i+1)
-    else
-      push_token beg i []
-  and loop_on_whitespace beg i =
-    if i < String.length str then
-      if str.[i] != ' ' then
-	push_whitespace beg i (loop i (i+1))
-      else
-	loop_on_whitespace beg (i+1)
-    else
-      push_whitespace beg i []
-  in
-  loop 0 0
-
 (* Interpret notations with a recursive component *)
 
 let out_nt = function NonTerminal x -> x | _ -> assert false
@@ -284,17 +254,6 @@ let quote_notation_token x =
   if (n > 0 && norm) || (n > 2 && x.[0] == '\'') then "'"^x^"'"
   else x
 
-let rec raw_analyze_notation_tokens = function
-  | []    -> []
-  | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
-  | String "_" :: _ -> user_err Pp.(str "_ must be quoted.")
-  | String x :: sl when CLexer.is_ident x ->
-      NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
-  | String s :: sl ->
-      Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl
-  | WhiteSpace n :: sl ->
-      Break n :: raw_analyze_notation_tokens sl
-
 let is_numeral symbs =
   match List.filter (function Break _ -> false | _ -> true) symbs with
   | ([Terminal "-"; Terminal x] | [Terminal x]) ->
@@ -315,8 +274,8 @@ let rec get_notation_vars onlyprint = function
   | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl
   | SProdList _ :: _ -> assert false
 
-let analyze_notation_tokens ~onlyprint l =
-  let l = raw_analyze_notation_tokens l in
+let analyze_notation_tokens ~onlyprint ntn =
+  let l = decompose_raw_notation ntn in
   let vars = get_notation_vars onlyprint l in
   let recvars,l = interp_list_parser [] l in
   recvars, List.subtract Id.equal vars (List.map snd recvars), l
@@ -509,9 +468,8 @@ let warn_format_break =
          (fun () ->
           strbrk "Discarding format implicitly indicated by multiple spaces in notation because an explicit format modifier is given.")
 
-
 let rec split_format_at_ldots hd = function
-  | (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string ldots_var) -> loc, List.rev hd, fmt
+  | (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string Notation_ops.ldots_var) -> loc, List.rev hd, fmt
   | u :: fmt ->
       check_no_ldots_in_box u;
       split_format_at_ldots (u::hd) fmt
@@ -1163,8 +1121,7 @@ let compute_syntax_data df modifiers =
   let onlyparse = mods.only_parsing in
   if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
   let assoc = Option.append mods.assoc (Some NonA) in
-  let toks = split_notation_string df in
-  let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint toks in
+  let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
   let _ = check_useless_entry_types recvars mainvars mods.etyps in
   let _ = check_binder_type recvars mods.etyps in
 
@@ -1385,8 +1342,7 @@ let add_notation_in_scope local df env c mods scope =
   sd.info
 
 let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
-  let dfs = split_notation_string df in
-  let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint dfs in
+  let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
   (* Recover types of variables and pa/pp rules; redeclare them if needed *)
   let i_typs, onlyprint = if not (is_numeral symbs) then begin
     let sy = recover_notation_syntax (make_notation_key symbs) in
@@ -1462,8 +1418,7 @@ let add_notation local env c ((loc,df),modifiers) sc =
 
 let add_notation_extra_printing_rule df k v =
   let notk = 
-    let dfs = split_notation_string df in
-    let _,_, symbs = analyze_notation_tokens ~onlyprint:true dfs in
+    let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
     make_notation_key symbs in
   Notation.add_notation_extra_printing_rule notk k v