+class interpErrorModel =
+ let cols = new GTree.column_list in
+ let id_col = cols#add Gobject.Data.string in
+ let dsc_col = cols#add Gobject.Data.string in
+ let interp_no_col = cols#add Gobject.Data.int in
+ let tree_store = GTree.tree_store cols in
+ let id_renderer = GTree.cell_renderer_text [], ["text", id_col] in
+ let dsc_renderer = GTree.cell_renderer_text [], ["text", dsc_col] in
+ let id_view_col = GTree.view_column ~renderer:id_renderer () in
+ let dsc_view_col = GTree.view_column ~renderer:dsc_renderer () in
+ fun tree_view choices ->
+ object
+ initializer
+ tree_view#set_model (Some (tree_store :> GTree.model));
+ ignore (tree_view#append_column id_view_col);
+ ignore (tree_view#append_column dsc_view_col);
+ let name_of_interp =
+ (* try to find a reasonable name for an interpretation *)
+ let idx = ref 0 in
+ fun interp ->
+ try
+ let _,_,y = List.find (fun (_,x,y) -> x="0") interp in y
+ with Not_found ->
+ incr idx; string_of_int !idx
+ in
+ tree_store#clear ();
+ let idx = ref ~-1 in
+ List.iter
+ (fun pass,env,_,_,_ ->
+ incr idx;
+ let interp_row = tree_store#append () in
+ tree_store#set ~row:interp_row ~column:id_col
+ ("Pass " ^ string_of_int pass ^
+ "; Interpretation " ^ name_of_interp env);
+ tree_store#set ~row:interp_row ~column:interp_no_col !idx;
+ List.iter
+ (fun (_, id, dsc) ->
+ let row = tree_store#append ~parent:interp_row () in
+ tree_store#set ~row ~column:id_col id;
+ tree_store#set ~row ~column:dsc_col dsc;
+ tree_store#set ~row ~column:interp_no_col !idx)
+ env)
+ choices
+
+ method get_interp_no tree_path =
+ let iter = tree_store#get_iter tree_path in
+ tree_store#get ~row:iter ~column:interp_no_col
+ end
+
+
+let rec interactive_error_interp ?(all_passes=false) source_buffer notify_exn
+ offset errorll
+=
+ let errorll' =
+ if all_passes then errorll else List.rev (List.tl (List.tl (List.rev errorll))) in
+ let choices =
+ let pass = ref 0 in
+ List.flatten
+ (List.map
+ (fun l ->
+ incr pass;
+ List.map (fun (env,diff,offset,msg) -> !pass, env, diff, offset, msg) l
+ ) errorll') in
+ let choices_eq (_,e1,_,_,_) (_,e2,_,_,_) = e1 = e2 in
+ let choices_compare (_,e1,_,_,_) (_,e2,_,_,_) = compare e1 e2 in
+ (* Here we are doing a stable sort and list_uniq returns the latter
+ "equal" element. I.e. we are showing the error corresponding to the
+ most advanced disambiguation pass *)
+ let choices =
+ HExtlib.list_uniq ~eq:choices_eq
+ (List.stable_sort choices_compare choices)
+ in
+ match choices with
+ [] -> assert false
+ | [_,env,diff,loffset,msg] ->
+ notify_exn
+ (GrafiteDisambiguator.DisambiguationError
+ (offset,[[env,diff,loffset,msg]]));
+ | _::_ ->
+ let dialog = new disambiguationErrors () in
+ dialog#check_widgets ();
+ if all_passes then
+ dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
+ let model = new interpErrorModel dialog#treeview choices in
+ dialog#disambiguationErrors#set_title "Interpretation choice";
+ dialog#disambiguationErrorsLabel#set_label "Choose an interpretation:";
+ ignore (dialog#treeview#connect#cursor_changed (fun _ ->
+ let tree_path =
+ match fst (dialog#treeview#get_cursor ()) with
+ None -> assert false
+ | Some tp -> tp in
+ let idx = model#get_interp_no tree_path in
+ let _,env,diff,loffset,msg = List.nth choices idx in
+ let script = MatitaScript.current () in
+ let error_tag = script#error_tag in
+ source_buffer#remove_tag error_tag
+ ~start:source_buffer#start_iter
+ ~stop:source_buffer#end_iter;
+ notify_exn
+ (GrafiteDisambiguator.DisambiguationError
+ (offset,[[env,diff,loffset,msg]]))
+ ));
+ let return _ =
+ dialog#disambiguationErrors#destroy ();
+ GMain.Main.quit ()
+ in
+ let fail _ = return () in
+ ignore (dialog#disambiguationErrors#event#connect#delete (fun _ -> true));
+ connect_button dialog#disambiguationErrorsOkButton (fun _ -> return ());
+ connect_button dialog#disambiguationErrorsMoreErrors
+ (fun _ -> return () ;
+ interactive_error_interp ~all_passes:true source_buffer notify_exn offset
+ errorll);
+ connect_button dialog#disambiguationErrorsCancelButton fail;
+ dialog#disambiguationErrors#show ();
+ GtkThread.main ()
+
+