diff options
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 43 |
1 files changed, 22 insertions, 21 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index feeca6075..8f64f5519 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -15,6 +15,7 @@ open Names open Constrexpr open Constrexpr_ops open Notation_term +open Notation_gram open Notation_ops open Ppextend open Extend @@ -76,22 +77,22 @@ let pr_grammar = function pr_entry Pcoq.Constr.pattern | "vernac" -> str "Entry vernac_control is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.vernac_control ++ + pr_entry Pvernac.Vernac_.vernac_control ++ str "Entry command is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.command ++ + pr_entry Pvernac.Vernac_.command ++ str "Entry syntax is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.syntax ++ + pr_entry Pvernac.Vernac_.syntax ++ str "Entry gallina is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.gallina ++ + pr_entry Pvernac.Vernac_.gallina ++ str "Entry gallina_ext is" ++ fnl () ++ - pr_entry Pcoq.Vernac_.gallina_ext + pr_entry Pvernac.Vernac_.gallina_ext | name -> pr_registered_grammar name (**********************************************************************) (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) -let parse_format ({CAst.loc;v=str} : Misctypes.lstring) = +let parse_format ({CAst.loc;v=str} : lstring) = let len = String.length str in (* TODO: update the line of the location when the string contains newlines *) let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in @@ -709,7 +710,7 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec = pr_level ntn prec ++ str ".") type syntax_extension = { - synext_level : Notation_term.level; + synext_level : Notation_gram.level; synext_notation : notation; synext_notgram : notation_grammar; synext_unparsing : unparsing list; @@ -728,8 +729,8 @@ let check_and_extend_constr_grammar ntn rule = let ntn_for_grammar = rule.notgram_notation in if String.equal ntn ntn_for_grammar then raise Not_found; let prec = rule.notgram_level in - let oldprec = Notation.level_of_notation ntn_for_grammar in - if not (Notation.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; + let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in + if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec; with Not_found -> Egramcoq.extend_constr_grammar rule @@ -738,16 +739,16 @@ let cache_one_syntax_extension se = let prec = se.synext_level in let onlyprint = se.synext_notgram.notgram_onlyprinting in try - let oldprec = Notation.level_of_notation ntn in - if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; + let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in + if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> if is_active_compat se.synext_compat then begin (* Reserve the notation level *) - Notation.declare_notation_level ntn prec; + Notgram_ops.declare_notation_level ntn prec ~onlyprint; (* Declare the parsing rule *) if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; (* Declare the notation rule *) - Notation.declare_notation_rule ntn + declare_notation_rule ntn ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram end @@ -791,7 +792,7 @@ type notation_modifier = { only_parsing : bool; only_printing : bool; compat : Flags.compat_version option; - format : Misctypes.lstring option; + format : lstring option; extra : (string * string) list; } @@ -1061,7 +1062,7 @@ let find_precedence lev etyps symbols onlyprint = [],Option.get lev let check_curly_brackets_notation_exists () = - try let _ = Notation.level_of_notation "{ _ }" in () + try let _ = Notgram_ops.level_of_notation "{ _ }" in () with Not_found -> user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\ specially and require that the notation \"{ _ }\" is already reserved.") @@ -1103,7 +1104,7 @@ module SynData = struct only_parsing : bool; only_printing : bool; compat : Flags.compat_version option; - format : Misctypes.lstring option; + format : lstring option; extra : (string * string) list; (* XXX: Callback to printing, must remove *) @@ -1274,10 +1275,10 @@ exception NoSyntaxRule let recover_notation_syntax ntn = try - let prec = Notation.level_of_notation ntn in - let pp_rule,_ = Notation.find_notation_printing_rule ntn in - let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in - let pa_rule = Notation.find_notation_parsing_rules ntn in + let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in + let pp_rule,_ = find_notation_printing_rule ntn in + let pp_extra_rules = find_notation_extra_printing_rules ntn in + let pa_rule = find_notation_parsing_rules ntn in { synext_level = prec; synext_notation = ntn; synext_notgram = pa_rule; @@ -1444,7 +1445,7 @@ let add_notation_extra_printing_rule df k v = let notk = let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in make_notation_key symbs in - Notation.add_notation_extra_printing_rule notk k v + add_notation_extra_printing_rule notk k v (* Infix notations *) |