code for DisambiguationErrors simplified

Still not working (since matita 0.99x?)

diff --git a/matita/matita/matita.ui b/matita/matita/matita.ui
index 731419c1c8c6c4c3aa1257f85f39c29d1ef84dca..6e8481589cba99e67c3f2cebae76016db891f627 100644 (file)
--- a/matita/matita/matita.ui
+++ b/matita/matita/matita.ui
@@ -759,106 +759,7 @@
           <object class="GtkButtonBox" id="hbuttonbox2">
             <property name="visible">True</property>
             <property name="can_focus">False</property>
-            <property name="layout_style">end</property>
-            <child>
-              <object class="GtkButton" id="button6">
-                <property name="label">gtk-help</property>
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="receives_default">False</property>
-                <property name="use_stock">True</property>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">0</property>
-              </packing>
-            </child>
-            <child>
-              <object class="GtkButton" id="disambiguationErrorsMoreErrors">
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="receives_default">False</property>
-                <child>
-                  <object class="GtkAlignment" id="alignment18">
-                    <property name="visible">True</property>
-                    <property name="can_focus">False</property>
-                    <property name="xscale">0</property>
-                    <property name="yscale">0</property>
-                    <child>
-                      <object class="GtkBox" id="hbox29">
-                        <property name="visible">True</property>
-                        <property name="can_focus">False</property>
-                        <property name="spacing">2</property>
-                        <child>
-                          <object class="GtkImage" id="image926">
-                            <property name="visible">True</property>
-                            <property name="can_focus">False</property>
-                            <property name="stock">gtk-zoom-in</property>
-                          </object>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                            <property name="position">0</property>
-                          </packing>
-                        </child>
-                        <child>
-                          <object class="GtkLabel" id="label28">
-                            <property name="visible">True</property>
-                            <property name="can_focus">False</property>
-                            <property name="label">More</property>
-                            <property name="use_underline">True</property>
-                          </object>
-                          <packing>
-                            <property name="expand">False</property>
-                            <property name="fill">False</property>
-                            <property name="position">1</property>
-                          </packing>
-                        </child>
-                      </object>
-                    </child>
-                  </object>
-                </child>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">1</property>
-              </packing>
-            </child>
-            <child>
-              <object class="GtkButton" id="disambiguationErrorsCancelButton">
-                <property name="label">gtk-cancel</property>
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="has_default">True</property>
-                <property name="receives_default">False</property>
-                <property name="use_stock">True</property>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">2</property>
-              </packing>
-            </child>
-            <child>
-              <object class="GtkButton" id="disambiguationErrorsOkButton">
-                <property name="label">gtk-ok</property>
-                <property name="visible">True</property>
-                <property name="can_focus">True</property>
-                <property name="can_default">True</property>
-                <property name="receives_default">False</property>
-                <property name="use_stock">True</property>
-              </object>
-              <packing>
-                <property name="expand">False</property>
-                <property name="fill">False</property>
-                <property name="position">3</property>
-              </packing>
-            </child>
+            <property name="layout_style">spread</property>
           </object>
           <packing>
             <property name="expand">False</property>
@@ -888,9 +789,11 @@
               <object class="GtkScrolledWindow" id="scrolledwindow12">
                 <property name="visible">True</property>
                 <property name="can_focus">True</property>
+                <property name="vexpand">True</property>
                 <property name="shadow_type">in</property>
                 <child>
                   <object class="GtkTreeView" id="treeview">
+                    <property name="height_request">717</property>
                     <property name="visible">True</property>
                     <property name="can_focus">True</property>
                     <property name="headers_visible">False</property>
@@ -915,12 +818,6 @@
         </child>
       </object>
     </child>
-    <action-widgets>
-      <action-widget response="-11">button6</action-widget>
-      <action-widget response="-6">disambiguationErrorsMoreErrors</action-widget>
-      <action-widget response="-6">disambiguationErrorsCancelButton</action-widget>
-      <action-widget response="-5">disambiguationErrorsOkButton</action-widget>
-    </action-widgets>
   </object>
   <object class="GtkWindow" id="FindReplWin">
     <property name="can_focus">False</property>

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index b294af25d45a5ed7c46a1e0dd991a317c39c82c8..e001f1db04661c8f9d884075e15c850b066f0037 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -319,8 +319,10 @@ let interactive_error_interp ~all_passes
             (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
     | _::_ ->
        let dialog = new disambiguationErrors () in
-       if all_passes then
-        dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
+   dialog#toplevel#add_button "Fix this interpretation" `OK;
+   dialog#toplevel#add_button "Close" `DELETE_EVENT;
+   if not all_passes then
+    dialog#toplevel#add_button "More errors" `HELP; (* HELP means MORE *)
        let model = new interpErrorModel dialog#treeview choices in
        dialog#disambiguationErrors#set_title "Disambiguation error";
        dialog#disambiguationErrorsLabel#set_label
@@ -352,57 +354,50 @@ let interactive_error_interp ~all_passes
             (MultiPassDisambiguator.DisambiguationError
               (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
            ));
-       let return _ =
-         dialog#disambiguationErrors#destroy ();
-         GMain.Main.quit ()
+   dialog#toplevel#show ();
+   ignore(dialog#toplevel#connect#response (function
+    | `OK ->
+       let tree_path =
+        match fst (dialog#treeview#get_cursor ()) with
+           None -> assert false
+        | Some tp -> tp in
+       let idx1,idx2,idx3 = model#get_interp_no tree_path in
+       let diff =
+        match idx2,idx3 with
+           Some idx2, Some idx3 ->
+            let _,lll = List.nth choices idx1 in
+            let _,envs_and_diffs,_,_ = List.nth lll idx2 in
+            let _,_,diff = List.nth envs_and_diffs idx3 in
+             diff
+         | _,_ -> assert false
        in
-       let fail _ = return () in
-       ignore(dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
-       connect_button dialog#disambiguationErrorsOkButton
-        (fun _ ->
-          let tree_path =
-           match fst (dialog#treeview#get_cursor ()) with
-              None -> assert false
-           | Some tp -> tp in
-          let idx1,idx2,idx3 = model#get_interp_no tree_path in
-          let diff =
-           match idx2,idx3 with
-              Some idx2, Some idx3 ->
-               let _,lll = List.nth choices idx1 in
-               let _,envs_and_diffs,_,_ = List.nth lll idx2 in
-               let _,_,diff = List.nth envs_and_diffs idx3 in
-                diff
-            | _,_ -> assert false
-          in
-           let newtxt =
-            String.concat "\n"
-             ("" ::
-               List.map
-                (fun k,desc -> 
-                  let alias =
-                   match k with
-                   | DisambiguateTypes.Id id ->
-                       GrafiteAst.Ident_alias (id, desc)
-                   | DisambiguateTypes.Symbol (symb, i)-> 
-                       GrafiteAst.Symbol_alias (symb, i, desc)
-                   | DisambiguateTypes.Num i ->
-                       GrafiteAst.Number_alias (i, desc)
-                  in
-                   GrafiteAstPp.pp_alias alias)
-                diff) ^ "\n"
-           in
-            source_buffer#insert
-             ~iter:
-               (source_buffer#get_iter_at_mark
-                (`NAME "beginning_of_statement")) newtxt ;
-            return ()
-        );
-       connect_button dialog#disambiguationErrorsMoreErrors
-        (fun _ -> return () ; raise UseLibrary);
-       connect_button dialog#disambiguationErrorsCancelButton fail;
-       dialog#disambiguationErrors#show ();
-       GtkThread.main ()
-
+        let newtxt =
+         String.concat "\n"
+          ("" ::
+            List.map
+             (fun k,desc -> 
+               let alias =
+                match k with
+                | DisambiguateTypes.Id id ->
+                    GrafiteAst.Ident_alias (id, desc)
+                | DisambiguateTypes.Symbol (symb, i)-> 
+                    GrafiteAst.Symbol_alias (symb, i, desc)
+                | DisambiguateTypes.Num i ->
+                    GrafiteAst.Number_alias (i, desc)
+               in
+                GrafiteAstPp.pp_alias alias)
+             diff) ^ "\n"
+        in
+         source_buffer#insert
+          ~iter:
+            (source_buffer#get_iter_at_mark
+             (`NAME "beginning_of_statement")) newtxt ;
+         dialog#toplevel#destroy ()
+    | `HELP (* HELP MEANS MORE *) ->
+        dialog#toplevel#destroy ();
+        raise UseLibrary
+    | `DELETE_EVENT -> dialog#toplevel#destroy ()
+    | _ -> assert false))
 
 class gui () =
     (* creation order _is_ relevant for windows placement *)