diff options
| -rw-r--r-- | kernel/names.ml | 9 | ||||
| -rw-r--r-- | kernel/names.mli | 6 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 18 |
3 files changed, 25 insertions, 8 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 4ccf5b60a..480b37e89 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -33,9 +33,9 @@ struct let hash = String.hash - let check_soft x = + let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then Errors.error x else Pp.msg_warning (str x) + if fatal then Errors.error x else if warn then Pp.msg_warning (str x) in Option.iter iter (Unicode.ident_refutation x) @@ -48,6 +48,11 @@ struct let s = String.copy s in String.hcons s + let of_string_soft s = + let () = check_soft ~warn:false s in + let s = String.copy s in + String.hcons s + let to_string id = String.copy id let print id = str id diff --git a/kernel/names.mli b/kernel/names.mli index d82043da1..92ee58f26 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -29,7 +29,11 @@ sig val of_string : string -> t (** Converts a string into an identifier. May raise [UserError _] if the - string is not valid. *) + string is not valid, or echo a warning if it contains invalid identifier + characters. *) + + val of_string_soft : string -> t + (** Same as {!of_string} except that no warning is ever issued. *) val to_string : t -> string (** Converts a identifier into an string. *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c8eff59b1..639ec1e6e 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -62,11 +62,19 @@ let rec make_tags = function | [] -> [] let make_fresh_key = - let id = Summary.ref ~name:"Tactic Notation counter" 0 in - fun () -> KerName.make - (Safe_typing.current_modpath (Global.safe_env ())) - (Global.current_dirpath ()) - (incr id; Label.make ("_" ^ string_of_int !id)) + let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in + fun () -> + let cur = incr id; !id in + let lbl = Id.of_string ("_" ^ string_of_int cur) in + let kn = Lib.make_kn lbl in + let (mp, dir, _) = KerName.repr kn in + (** We embed the full path of the kernel name in the label so that the + identifier should be unique. This ensures that including two modules + together won't confuse the corresponding labels. *) + let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i" + (ModPath.to_string mp) (DirPath.to_string dir) cur) + in + KerName.make mp dir (Label.of_id lbl) type tactic_grammar_obj = { tacobj_key : KerName.t; |