From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 23 Jan 2004 16:39:35 +0000 (+0000)
Subject: moved environmentP3 in cic_textual_parser2 and reshaped interface
X-Git-Tag: V_0_2_3~159
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f7dbdfa37be6a1135df8169557eab5c92c485e2;p=helm.git

moved environmentP3 in cic_textual_parser2 and reshaped interface
---

diff --git a/helm/gTopLevel/chosenTermEditor.mli b/helm/gTopLevel/chosenTermEditor.mli
index 962aa0532..ebd9a95e6 100644
--- a/helm/gTopLevel/chosenTermEditor.mli
+++ b/helm/gTopLevel/chosenTermEditor.mli
@@ -5,7 +5,7 @@ class type term_editor =
     method get_metasenv_and_term :
       context:Cic.context ->
       metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
-    method environment : DisambiguatingParser.Environment.t ref
+    method environment : DisambiguatingParser.EnvironmentP3.t ref
     method reset : unit
     method set_term : string -> unit
   end
diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml
index 057cacb42..8ce12c045 100644
--- 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
diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli
index 6edb84239..397799548 100644
--- a/helm/gTopLevel/disambiguatingParser.mli
+++ b/helm/gTopLevel/disambiguatingParser.mli
@@ -25,10 +25,10 @@
 
 exception NoWellTypedInterpretation
 
-module Environment :
+module EnvironmentP3 :
  sig
   type t
-  val empty : t
+  val empty : string
   val to_string : t -> string
   val of_string : string -> t
  end
@@ -40,8 +40,8 @@ module Make (C : Disambiguate_types.Callbacks) :
       Cic.context ->
       Cic.metasenv ->
       string ->
-      Environment.t ->  (* previous interpretation status *)
-        Environment.t *                   (* new interpretation status *)
+      EnvironmentP3.t ->  (* previous interpretation status *)
+        EnvironmentP3.t *                   (* new interpretation status *)
         Cic.metasenv *                  (* new metasenv *)
         Cic.term                        (* disambiguated term *)
   end
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 76ebe6cc6..8932d21a8 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -746,12 +746,12 @@ let edit_aliases () =
   (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
   ignore
    (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
-     (DisambiguatingParser.Environment.to_string !id_to_uris)) ;
+     (DisambiguatingParser.EnvironmentP3.to_string !id_to_uris)) ;
   window#show () ;
   GtkThread.main ();
   if !chosen then
    id_to_uris :=
-    DisambiguatingParser.Environment.of_string (input#buffer#get_text ())
+    DisambiguatingParser.EnvironmentP3.of_string (input#buffer#get_text ())
 ;;
 
 let proveit () =
diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml
index ca5cca601..668bf1502 100644
--- a/helm/gTopLevel/termEditor.ml
+++ b/helm/gTopLevel/termEditor.ml
@@ -48,7 +48,7 @@ class type term_editor =
    method reset : unit
    (* The input of set_term is unquoted *)
    method set_term : string -> unit
-   method environment : DisambiguatingParser.Environment.t ref
+   method environment : DisambiguatingParser.EnvironmentP3.t ref
  end
 
 module Make(C:Disambiguate_types.Callbacks) =
@@ -61,7 +61,9 @@ module Make(C:Disambiguate_types.Callbacks) =
    =
     let environment =
      match share_environment_with with
-        None -> ref DisambiguatingParser.Environment.empty
+        None -> ref
+          (DisambiguatingParser.EnvironmentP3.of_string
+            DisambiguatingParser.EnvironmentP3.empty)
       | Some obj -> obj#environment
     in
     let input = GText.view ~editable:true ?width ?height ?packing () in
diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli
index e9e725ed2..67b076505 100644
--- a/helm/gTopLevel/termEditor.mli
+++ b/helm/gTopLevel/termEditor.mli
@@ -33,7 +33,7 @@ class type term_editor =
      metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
    method reset : unit
    method set_term : string -> unit
-   method environment : DisambiguatingParser.Environment.t ref
+   method environment : DisambiguatingParser.EnvironmentP3.t ref
  end
 
 module Make (C : Disambiguate_types.Callbacks) :