- Added DisambiguatingParser (that abstracts both the parser and the

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index d54236fd8b221107684230b740e6d3b03c110bba..76ebe6cc6f453ed657e0ac683f9f1773302eb5b7 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -719,7 +719,7 @@ let load_unfinished_proof () =
 
 let edit_aliases () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let id_to_uris = inputt#id_to_uris in
+ let id_to_uris = inputt#environment in
  let chosen = ref false in
  let window =
   GWindow.window
@@ -744,66 +744,14 @@ let edit_aliases () =
  ignore (cancelb#connect#clicked window#destroy) ;
  ignore
   (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
- let resolve_id = !id_to_uris in
   ignore
    (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
-    (Disambiguate_types.Environment.fold
-      (fun i v s ->
-        match i with
-        | Disambiguate_types.Id id -> s ^ sprintf "alias %s %s\n" id (fst v)
-        | _ -> "")
-      resolve_id "")) ;
-(*
-        (function v ->
-          let uri =
-           match resolve_id v with
-              None -> assert false
-            | Some (CicTextualParser0.Uri uri) -> uri
-            | Some (CicTextualParser0.Term _)
-            | Some CicTextualParser0.Implicit -> assert false
-          in
-           "alias " ^
-            (match v with
-                CicTextualParser0.Id id -> id
-              | CicTextualParser0.Symbol (descr,_) ->
-                 (* CSC: To be implemented *)
-                 assert false
-            )^ " " ^ (string_of_cic_textual_parser_uri uri)
-        )
-*)
+     (DisambiguatingParser.Environment.to_string !id_to_uris)) ;
   window#show () ;
   GtkThread.main ();
   if !chosen then
-   let resolve_id =
-    let inputtext = input#buffer#get_text () in
-    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 -> TermEditor.empty_id_to_uris
-     in
-      aux 0
-   in
-    id_to_uris := resolve_id
+   id_to_uris :=
+    DisambiguatingParser.Environment.of_string (input#buffer#get_text ())
 ;;
 
 let proveit () =
@@ -1083,18 +1031,8 @@ exception AmbiguousInput;;
 
 (* A WIDGET TO ENTER CIC TERMS *)
 
-(*
-module ChosenTermEditor  = TexTermEditor;;
-module ChosenTextualParser0 = TexCicTextualParser0;;
-*)
-module ChosenTermEditor = TermEditor;;
-module ChosenTextualParser0 = CicTextualParser0;;
-
 module Callbacks =
  struct
-  let get_metasenv () = !ChosenTextualParser0.metasenv
-  let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
-
   let output_html ?append_NL = output_html ?append_NL (outputhtml ())
   let interactive_user_uri_choice =
    fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
@@ -1254,7 +1192,7 @@ let new_inductive () =
        TexTermEditor'.term_editor
         mqi_handle
         ~width:400 ~height:20 ~packing:scrolled_window#add 
-        ~share_id_to_uris_with:inputt ()
+        ~share_environment_with:inputt ()
         ~isnotempty_callback:
          (function b ->
            (*non_empty_type := b ;*)
@@ -1366,7 +1304,7 @@ let new_inductive () =
        TexTermEditor'.term_editor
         mqi_handle
         ~width:400 ~height:20 ~packing:scrolled_window#add
-        ~share_id_to_uris_with:inputt ()
+        ~share_environment_with:inputt ()
         ~isnotempty_callback:
          (function b ->
            (* (*non_empty_type := b ;*)
@@ -1513,18 +1451,14 @@ let new_proof () =
   TexTermEditor'.term_editor
    mqi_handle
    ~width:400 ~height:100 ~packing:scrolled_window#add
-   ~share_id_to_uris_with:inputt ()
+   ~share_environment_with:inputt ()
    ~isnotempty_callback:
     (function b ->
       non_empty_type := b ;
       okb#misc#set_sensitive (b && uri_entry#text <> ""))
  in
  let _ =
-let xxx = inputt#get_as_string in
-  newinputt#set_term xxx ;
-(*
-  newinputt#set_term inputt#get_as_string ;
-*)
+  newinputt#set_term inputt#get_as_string  ;
   inputt#reset in
  let _ =
   uri_entry#connect#changed