~refresh_uri_in_reference t, n)
type binding =
- | NoBinding
+ | NoBinding of string option (* name of Ast.Symbol associated to this literal *)
| Binding of string * Env.value_type
| Env of (string * Env.value_type) list
let rec aux (vl : NotationEnv.t) =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
- | NoBinding :: tl ->
+ | NoBinding csym :: tl ->
Gramext.action
(fun ((*_,*)(loc: Ast.location)) ->
let uri,desc =
try
+ let a,b = HExtlib.loc_of_floc loc in
CicNotationLexer.LocalizeEnv.find loc
!(status#notation_parser_db.loctable)
with Not_found -> None, None
in aux (("",(Env.NoType,
- Env.DisambiguationValue (loc,uri,desc)))::vl) tl)
+ Env.DisambiguationValue (csym,loc,uri,desc)))::vl) tl)
(* LUCA: DEFCON 3 BEGIN *)
| Binding (name, Env.TermType l) :: tl ->
Gramext.action
let rec aux acc =
function
[] -> List.rev acc
- | NoBinding :: tl -> aux acc tl
+ | NoBinding _ :: tl -> aux acc tl
| Env names :: tl -> aux (List.rev names @ acc) tl
| Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
in
assert false
and aux_literal status =
function
- | `Symbol (s,_) -> add_item_to_grammar status (`Sym s)
- | `Keyword (s,_) ->
+ | _,`Symbol (s,_) -> add_item_to_grammar status (`Sym s)
+ | _,`Keyword (s,_) ->
if not (List.mem s CicNotationLexer.initial_keywords)
then add_item_to_grammar status (`Kwd s)
else status
- | `Number _ -> status
+ | _,`Number _ -> status
and aux_layout status = function
| Ast.Sub (p1, p2) -> aux (aux status p1) p2
| Ast.Sup (p1, p2) -> aux (aux status p1) p2
| Ast.List0 (p, s)
| Ast.List1 (p, s) ->
let status =
- match s with None -> status | Some s' -> aux_literal status s'
+ match s with None -> status | Some s' -> aux_literal status (None,s')
in
aux status p
| _ -> assert false
assert false
and aux_literal =
function
- | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
- | `Keyword (s,_) ->
+ | csym,`Symbol (s,_) -> [NoBinding csym, gram_symbol status s]
+ | csym,`Keyword (s,_) ->
(* assumption: s will be registered as a keyword with the lexer *)
- [NoBinding, gram_keyword status s]
- | `Number (s,_) -> [NoBinding, gram_number s]
+ [NoBinding csym, gram_keyword status s]
+ | csym,`Number (s,_) -> [NoBinding csym, gram_number s]
and aux_layout = function
- | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2
- | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2
- | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\below "] @ aux p2
- | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\above "] @ aux p2
- | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\frac "] @ aux p2
- | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3
- | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\atop "] @ aux p2
- | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\over "] @ aux p2
+ | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sub "] @ aux p2
+ | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sup "] @ aux p2
+ | Ast.Below (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\below "] @ aux p2
+ | Ast.Above (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\above "] @ aux p2
+ | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\frac "] @ aux p2
+ | Ast.InfRule (p1, p2, p3) -> [NoBinding None, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3
+ | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\atop "] @ aux p2
+ | Ast.Over (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\over "] @ aux p2
| Ast.Root (p1, p2) ->
- [NoBinding, gram_symbol status "\\root "] @ aux p2
- @ [NoBinding, gram_symbol status "\\of "] @ aux p1
- | Ast.Sqrt p -> [NoBinding, gram_symbol status "\\sqrt "] @ aux p
+ [NoBinding None, gram_symbol status "\\root "] @ aux p2
+ @ [NoBinding None, gram_symbol status "\\of "] @ aux p1
+ | Ast.Sqrt p -> [NoBinding None, gram_symbol status "\\sqrt "] @ aux p
| Ast.Break -> []
| Ast.Box (_, pl) -> List.flatten (List.map aux pl)
| Ast.Group pl -> List.flatten (List.map aux pl)
| n = NUMBER -> `Number (n,(None,None))
]
];
+ rliteral: [
+ [ csymname = OPT [ "ref" ; csymname = CSYMBOL ->
+ prerr_endline ("parser in rliteral (ref " ^ csymname ^ ")");
+ csymname ];
+ lit = literal ->
+ csymname, lit
+ ]
+ ];
sep: [ [ "sep"; sep = literal -> sep ] ];
l1_magic_pattern: [
[ "list0"; p = l1_simple_pattern; sep = OPT sep ->
return_term_of_level loc (fun l -> Ast.Magic (m l))
| v = l1_pattern_variable ->
return_term_of_level loc (fun _ -> Ast.Variable v)
- | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l)
+ | l = rliteral -> return_term_of_level loc (fun _ -> Ast.Literal l)
]
];
END