moved environmentP3 in cic_textual_parser2 and reshaped interface

diff --git a/helm/gTopLevel/chosenTermEditor.mli b/helm/gTopLevel/chosenTermEditor.mli
index 962aa0532c36f5648665d1e914f07ec08a41d26e..ebd9a95e664e61d80e73cf85a3e30f1d35911ed1 100644 (file)
--- 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 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

diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli
index 6edb842399971bd37f73bd0d20229fc4e7b1371d..397799548b20480c2e1c1233f25f042d849c590d 100644 (file)
--- 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 76ebe6cc6f453ed657e0ac683f9f1773302eb5b7..8932d21a86eec829cc62fb0f32dd38bd4bcc7a33 100644 (file)
--- 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 ca5cca601e615c6daf96b5bdcaff3f525852e1d3..668bf1502a8e0065e98193629ad95b9d4a2d97f0 100644 (file)
--- 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 e9e725ed2a635495b140075d6960fb9239c3d3d1..67b076505cf347954519244424b7af27ed4fc0e1 100644 (file)
--- 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) :