X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=cf1c0de4df94a203ac73c6ea0ab04be63e8c0642;hb=94a75f971149efd44cde424b6aad38aacbb3c250;hp=2a607d9fcf0cac59bf7a538d90b82c8239700952;hpb=f69398e899452aaf8490d7f1a116e30163426bc7;p=helm.git diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 2a607d9fc..cf1c0de4d 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -129,6 +129,127 @@ let ask_unsaved parent = "Do you want to save the script before continuing?") () +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 () + + (** Selection handling * Two clipboards are used: "clipboard" and "primary". * "primary" is used by X, when you hit the middle button mouse is content is @@ -422,7 +543,9 @@ class gui () = main#buttonsToolbar#misc#set_sensitive true; develList#buttonsHbox#misc#set_sensitive true; main#scriptMenu#misc#set_sensitive true; - source_view#set_editable true + source_view#set_editable true; + (*The next line seems sufficient to avoid some unknown race condition *) + GtkThread.sync (fun () -> ()) () in let worker_thread = ref None in let notify_exn exn = @@ -462,9 +585,13 @@ class gui () = try f (); unlock_world () - with exc -> - unlock_world (); - notify_exn exc + with + | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> + interactive_error_interp source_buffer notify_exn offset errorll ; + unlock_world () + | exc -> + notify_exn exc; + unlock_world () in worker_thread := Some (Thread.create thread_main ()) in let kill_worker = @@ -1115,11 +1242,6 @@ class gui () = dialog#check_widgets (); dialog - method newRecordDialog () = - let dialog = new recordChoiceDialog () in - dialog#check_widgets (); - dialog - method newConfirmationDialog () = let dialog = new confirmationDialog () in dialog#check_widgets (); @@ -1324,36 +1446,6 @@ class interpModel = tree_store#get ~row:iter ~column:interp_no_col end -let interactive_interp_choice () = - fun text prefix_len choices -> - let gui = instance () in - assert (choices <> []); - let dialog = gui#newRecordDialog () in - let model = new interpModel dialog#recordChoiceTreeView choices in - dialog#recordChoiceDialog#set_title "Interpretation choice"; - dialog#recordChoiceDialogLabel#set_label "Choose an interpretation:"; - let interp_no = ref None in - let return _ = - dialog#recordChoiceDialog#destroy (); - GMain.Main.quit () - in - let fail _ = interp_no := None; return () in - ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#recordChoiceOkButton (fun _ -> - match !interp_no with None -> () | Some _ -> return ()); - connect_button dialog#recordChoiceCancelButton fail; - ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ -> - interp_no := Some (model#get_interp_no path); - return ())); - let selection = dialog#recordChoiceTreeView#selection in - ignore (selection#connect#changed (fun _ -> - match selection#get_selected_rows with - | [path] -> interp_no := Some (model#get_interp_no path) - | _ -> assert false)); - dialog#recordChoiceDialog#show (); - GtkThread.main (); - (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel) - let interactive_string_choice text prefix_len ?(title = "") ?(msg = "") () ~id locs uris =