diff options
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
| -rw-r--r-- | plugins/syntax/string_syntax.ml | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 2421cc12..7478c1e9 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open Globnames open Ascii_syntax_plugin.Ascii_syntax open Glob_term @@ -34,7 +35,7 @@ let glob_String = lazy (make_reference "String") let glob_EmptyString = lazy (make_reference "EmptyString") let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false open Lazy @@ -55,7 +56,7 @@ let uninterp_string (AnyGlobConstr r) = (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | GRef (z,_) when eq_gr z (force glob_EmptyString) -> + | GRef (z,_) when GlobRef.equal z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -63,10 +64,18 @@ let uninterp_string (AnyGlobConstr r) = with Non_closed_string -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "string_scope" - (string_path,["Coq";"Strings";"String"]) - interp_string - ([DAst.make @@ GRef (static_glob_String,None); - DAst.make @@ GRef (static_glob_EmptyString,None)], - uninterp_string, true) + let sc = "string_scope" in + register_string_interpretation sc (interp_string,uninterp_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = sc; + pt_interp_info = Uid sc; + pt_required = (string_path,["Coq";"Strings";"String"]); + pt_refs = [static_glob_String; static_glob_EmptyString]; + pt_in_match = true } |