moved environmentP3 in cic_textual_parser2 and reshaped interface

[helm.git] / helm / gTopLevel / disambiguatingParser.ml

diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml
index 057cacb4261496c3e6a262f45d4e830347d000b7..8ce12c04539c8d7fc9a05454643c6039f0cea135 100644 (file)
--- a/helm/gTopLevel/disambiguatingParser.ml
+++ b/helm/gTopLevel/disambiguatingParser.ml
@@ -25,50 +25,7 @@
 
 exception NoWellTypedInterpretation
 
-module Environment =
- struct
-  type t = Disambiguate_types.environment
-
-  let empty = Disambiguate_types.Environment.empty
-
-  let to_string env =
-prerr_endline "TODO: implement and move away" ;
-   Disambiguate_types.Environment.fold
-    (fun i v s ->
-      match i with
-      | Disambiguate_types.Id id ->s ^ Printf.sprintf "alias %s %s\n" id (fst v)
-      | _ -> "")
-    env ""
-
-  let of_string inputtext =
-   let regexpr =
-    let alfa = "[a-zA-Z_-]" in
-    let digit = "[0-9]" in
-    let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
-    let blanks = "\( \|\t\|\n\)+" in
-    let nonblanks = "[^ \t\n]+" in
-    let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
-     Str.regexp
-      ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
-   in
-    let rec aux n =
-     try
-      let n' = Str.search_forward regexpr inputtext n in
-       let id = Disambiguate_types.Id (Str.matched_group 2 inputtext) in
-       let uri = "cic:" ^ (Str.matched_group 5 inputtext) in
-        let resolve_id = aux (n' + 1) in
-         if Disambiguate_types.Environment.mem id resolve_id then
-          resolve_id
-         else
-           let term = Disambiguate.term_of_uri uri in
-           (Disambiguate_types.Environment.add id (uri, (fun _ _ _ -> term))
-             resolve_id)
-     with
-      Not_found -> Disambiguate_types.Environment.empty
-    in
-     aux 0
- end
-;;
+module EnvironmentP3 = Disambiguate_types.EnvironmentP3
 
 module Make (C : Disambiguate_types.Callbacks) =
  struct