From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 22 Dec 2018 14:32:24 +0000 (+0100)
Subject: code for DisambiguationErrors simplified
X-Git-Tag: make_still_working~229^2~1^2~25
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6f24874d21e1ba9187599d0817c9ac8185a2464e;p=helm.git
code for DisambiguationErrors simplified
Still not working (since matita 0.99x?)
---
diff --git a/matita/matita/matita.ui b/matita/matita/matita.ui
index 731419c1c..6e8481589 100644
--- 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 b294af25d..e001f1db0 100644
--- 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 *)