+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);
+ tree_store#clear ();
+ let idx = ref ~-1 in
+ List.iter
+ (fun passes,env,_,_,_ ->
+ incr idx;
+ let interp_row = tree_store#append () in
+ tree_store#set ~row:interp_row ~column:id_col
+ ("Passes " ^ String.concat " " (List.map string_of_int passes));
+ 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
+ (* 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 =
+ let choices_compare (_,e1,_,_,m1) (_,e2,_,_,m2) =
+ let m1 = Lazy.force m1 in
+ let m2 = Lazy.force m2 in
+ compare (e1,m1) (e2,m2) in
+ let choices_compare_by_passes (p1,_,_,_,_) (p2,_,_,_,_) = compare p1 p2 in
+ let rec uniq =
+ function
+ [] -> []
+ | h::[] -> [h]
+ | (p1,e1,_,_,_)::(p2,e2,d2,o2,m2)::tl when e1 = e2 ->
+ uniq ((p1@p2,e2,d2,o2,m2) :: tl)
+ | h1::tl -> h1 :: uniq tl
+ in
+ List.sort choices_compare_by_passes
+ (uniq (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 "Disambiguation error";
+ dialog#disambiguationErrorsLabel#set_label
+ "Click on an interpretation to see the corresponding error message:";
+ 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 ()
+
+