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
- List.assoc "0" interp
- with Not_found ->
- incr idx; string_of_int !idx
- in
tree_store#clear ();
let idx = ref ~-1 in
List.iter
- (fun _,interp,_,_ ->
+ (fun passes,env,_,_,_ ->
incr idx;
let interp_row = tree_store#append () in
tree_store#set ~row:interp_row ~column:id_col
- (name_of_interp interp);
+ ("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) ->
+ (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)
- interp)
+ env)
choices
method get_interp_no tree_path =
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
- (List.map
- (fun (choices,offset,msg) ->
- let textual_choices =
- List.map
- (fun (dom,(descr,_)) ->
- DisambiguateTypes.string_of_domain_item dom, descr
- ) choices
- in
- choices, textual_choices, offset, msg
- )
+ (fun l ->
+ incr pass;
+ List.map
+ (fun (env,diff,offset,msg) -> [!pass], env, diff, offset, msg) l
) errorll') in
- let choices_eq (_,c1,_,_) (_,c2,_,_) = c1 = c2 in
- let choices_compare (_,c1,_,_) (_,c2,_,_) = compare c1 c2 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)
+ 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
- | [interp,_,loffset,msg] ->
+ | [_,env,diff,loffset,msg] ->
notify_exn
(GrafiteDisambiguator.DisambiguationError
- (offset,[[interp,loffset,msg]]));
+ (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:";
+ 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 interp,_,loffset,msg = List.nth choices idx 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
~stop:source_buffer#end_iter;
notify_exn
(GrafiteDisambiguator.DisambiguationError
- (offset,[[interp,loffset,msg]]))
+ (offset,[[env,diff,loffset,msg]]))
));
let return _ =
dialog#disambiguationErrors#destroy ();