- s/id_to_uris/environment/

- bugfix: aliases work again

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index c3ef122db1d0ecc57251796ef2213c3e9f876340..7363abc2c02295d809fa86d54f6cf5d2e6af3b48 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -723,8 +723,8 @@ let load_unfinished_proof () =
 
 let edit_aliases () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let id_to_uris = inputt#environment in
- let chosen = ref false in
+ let disambiguation_env = inputt#environment in
+ let chosen_aliases = ref None in
  let window =
   GWindow.window
    ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
@@ -746,16 +746,28 @@ let edit_aliases () =
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  ignore (window#connect#destroy GMain.Main.quit) ;
  ignore (cancelb#connect#clicked window#destroy) ;
- ignore
-  (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
+ ignore (okb#connect#clicked (fun () ->
+    chosen_aliases := Some (input#buffer#get_text
+      ~start:input#buffer#start_iter ~stop:input#buffer#end_iter ());
+    window#destroy ()));
   ignore
    (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
-     (DisambiguatingParser.EnvironmentP3.to_string !id_to_uris)) ;
+     (DisambiguatingParser.EnvironmentP3.to_string !disambiguation_env ^ "\n"));
   window#show () ;
   GtkThread.main ();
-  if !chosen then
-   id_to_uris :=
-    DisambiguatingParser.EnvironmentP3.of_string (input#buffer#get_text ())
+  match !chosen_aliases with
+  | None -> ()
+  | Some raw_aliases ->
+      let new_disambiguation_env =
+        (try
+          DisambiguatingParser.EnvironmentP3.of_string raw_aliases
+        with e ->
+          output_html (outputhtml ())
+            (`Error (`T
+              ("Error while parsing aliases: " ^ Printexc.to_string e)));
+          !disambiguation_env)
+      in
+      disambiguation_env := new_disambiguation_env
 ;;
 
 let proveit () =
@@ -763,7 +775,7 @@ let proveit () =
  let module G = Gdome in
  let notebook = (rendering_window ())#notebook in
  let output = (rendering_window ())#output in
- let outputhtml = ((rendering_window ())#outputhtml (*: GHtml.xmhtml*)) in
+ let outputhtml = (rendering_window ())#outputhtml in
   try
    output#make_sequent_of_selected_term ;
    refresh_proof output ;
@@ -2812,10 +2824,9 @@ class rendering_window output (notebook : notebook) =
   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
  in
  let outputhtml =
-  new Ui_logger.html_logger
-   ~width:400 ~height: 100
-   ~packing:frame#add
-   ~show:true () in
+   new Ui_logger.html_logger
+    ~width:400 ~height: 100 ~show:true ~packing:frame#add ()
+ in
 object
  method outputhtml = outputhtml
  method inputt = inputt