X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=ff00ce27b69d925cc125a1220149cd9614a211a4;hb=94873bb61a663b4fca3dc6d07b7bb9f42122003e;hp=1f170cb912592b955a85a1294fcb2632f7571be1;hpb=1fe6285e012b840bd335eb49e0359d0411029c81;p=helm.git diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 1f170cb91..ff00ce27b 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -129,6 +129,262 @@ 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.caml 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: GTree.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 idx1 = ref ~-1 in + List.iter + (fun _,lll -> + incr idx1; + let loc_row = + if List.length choices = 1 then + None + else + (let loc_row = tree_store#append () in + begin + match lll with + [passes,envs_and_diffs,_] -> + tree_store#set ~row:loc_row ~column:id_col + ("Error location " ^ string_of_int (!idx1+1) ^ + ", error message " ^ string_of_int (!idx1+1) ^ ".1" ^ + " (in passes " ^ + String.concat " " (List.map string_of_int passes) ^ + ")"); + tree_store#set ~row:loc_row ~column:interp_no_col + (!idx1,Some 0,None); + | _ -> + tree_store#set ~row:loc_row ~column:id_col + ("Error location " ^ string_of_int (!idx1+1)); + tree_store#set ~row:loc_row ~column:interp_no_col + (!idx1,None,None); + end ; + Some loc_row) in + let idx2 = ref ~-1 in + List.iter + (fun passes,envs_and_diffs,_ -> + incr idx2; + let msg_row = + if List.length lll = 1 then + loc_row + else + let msg_row = tree_store#append ?parent:loc_row () in + (tree_store#set ~row:msg_row ~column:id_col + ("Error message " ^ string_of_int (!idx1+1) ^ "." ^ + string_of_int (!idx2+1) ^ + " (in passes " ^ + String.concat " " (List.map string_of_int passes) ^ + ")"); + tree_store#set ~row:msg_row ~column:interp_no_col + (!idx1,Some !idx2,None); + Some msg_row) in + let idx3 = ref ~-1 in + List.iter + (fun (passes,env,_) -> + incr idx3; + let interp_row = + match envs_and_diffs with + _::_::_ -> + let interp_row = tree_store#append ?parent:msg_row () in + tree_store#set ~row:interp_row ~column:id_col + ("Interpretation " ^ string_of_int (!idx3+1) ^ + " (in passes " ^ + String.concat " " (List.map string_of_int passes) ^ + ")"); + tree_store#set ~row:interp_row ~column:interp_no_col + (!idx1,Some !idx2,Some !idx3); + Some interp_row + | [_] -> msg_row + | [] -> assert false + in + 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 + (!idx1,Some !idx2,Some !idx3) + ) env + ) envs_and_diffs + ) lll ; + if List.length lll > 1 then + HExtlib.iter_option + (fun p -> tree_view#expand_row (tree_store#get_path p)) + loc_row + ) 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:GSourceView.source_buffer) notify_exn offset errorll += + let errorll' = + if all_passes then errorll else + (* We remove passes 1,2 and 5,6 *) + []::[]:: + List.tl (List.tl (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) -> + offset, [[!pass], [[!pass], env, diff], 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 (o1,_) (o2,_) = compare o1 o2 in + let choices_compare_by_passes (p1,_,_) (p2,_,_) = + compare p1 p2 in + let rec uniq = + function + [] -> [] + | h::[] -> [h] + | (o1,res1)::(o2,res2)::tl when o1 = o2 -> + let merge_by_name errors = + let merge_by_env errors = + let choices_compare_by_env (_,e1,_) (_,e2,_) = compare e1 e2 in + let choices_compare_by_passes (p1,_,_) (p2,_,_) = + compare p1 p2 in + let rec uniq_by_env = + function + [] -> [] + | h::[] -> [h] + | (p1,e1,_)::(p2,e2,d2)::tl when e1 = e2 -> + uniq_by_env ((p1@p2,e2,d2) :: tl) + | h1::tl -> h1 :: uniq_by_env tl + in + List.sort choices_compare_by_passes + (uniq_by_env (List.stable_sort choices_compare_by_env errors)) + in + let choices_compare_by_msg (_,_,m1) (_,_,m2) = + compare (Lazy.force m1) (Lazy.force m2) in + let rec uniq_by_msg = + function + [] -> [] + | h::[] -> [h] + | (p1,i1,m1)::(p2,i2,m2)::tl when Lazy.force m1 = Lazy.force m2 -> + uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2) :: tl) + | h1::tl -> h1 :: uniq_by_msg tl + in + List.sort choices_compare_by_msg + (uniq_by_msg (List.stable_sort choices_compare_by_msg errors)) + in + let res = merge_by_name (res1@res2) in + uniq ((o1,res) :: tl) + | h1::tl -> h1 :: uniq tl + in + List.map (fun o,l -> o,List.sort choices_compare_by_passes l) + (uniq (List.stable_sort choices_compare choices)) + in + match choices with + [] -> assert false + | [loffset,[_,envs_and_diffs,msg]] -> + let _,env,diff = List.hd envs_and_diffs in + 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 error to see the corresponding 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 idx1,idx2,idx3 = model#get_interp_no tree_path in + let loffset,lll = List.nth choices idx1 in + let _,envs_and_diffs,msg = + match idx2 with + Some idx2 -> List.nth lll idx2 + | None -> [],[],lazy "Multiple error messages. Please select one." in + let _,env,diff = + match idx3 with + Some idx3 -> List.nth envs_and_diffs idx3 + | None -> [],[],[] (* dymmy value, used *) 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 _ -> + 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,value -> + DisambiguatePp.pp_environment + (DisambiguateTypes.Environment.add k value + DisambiguateTypes.Environment.empty)) + 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 () ; + 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 @@ -415,17 +671,83 @@ class gui () = let lock_world _ = main#buttonsToolbar#misc#set_sensitive false; develList#buttonsHbox#misc#set_sensitive false; + main#scriptMenu#misc#set_sensitive false; source_view#set_editable false in let unlock_world _ = main#buttonsToolbar#misc#set_sensitive true; develList#buttonsHbox#misc#set_sensitive true; - source_view#set_editable true + main#scriptMenu#misc#set_sensitive true; + source_view#set_editable true; + (*The next line seems sufficient to avoid some unknown race condition *) + GtkThread.sync (fun () -> ()) () in - let locker f = + let worker_thread = ref None in + let notify_exn exn = + let floc, msg = MatitaExcPp.to_string exn in + begin + match floc with + None -> () + | Some floc -> + let (x, y) = HExtlib.loc_of_floc floc in + let script = MatitaScript.current () in + let locked_mark = script#locked_mark in + let error_tag = script#error_tag in + let baseoffset = + (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in + let x' = baseoffset + x in + let y' = baseoffset + y in + let x_iter = source_buffer#get_iter (`OFFSET x') in + let y_iter = source_buffer#get_iter (`OFFSET y') in + source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; + let id = ref None in + id := Some (source_buffer#connect#changed ~callback:(fun () -> + source_buffer#remove_tag error_tag + ~start:source_buffer#start_iter + ~stop:source_buffer#end_iter; + match !id with + | None -> assert false (* a race condition occurred *) + | Some id -> + (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id)); + source_buffer#place_cursor + (source_buffer#get_iter (`OFFSET x')); + end; + HLog.error msg in + let locker f () = + let thread_main = fun () -> lock_world (); - try f ();unlock_world () with exc -> unlock_world (); raise exc in + try + f (); + unlock_world () + 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 = + (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *) + let interrupt = ref None in + let old_callback = ref (function _ -> ()) in + let force_interrupt n = + (* This function is called just before the thread's timeslice ends *) + !old_callback n; + if Some(Thread.id(Thread.self())) = !interrupt then + (interrupt := None; raise Sys.Break) in + let _ = + match Sys.signal Sys.sigvtalrm (Sys.Signal_handle force_interrupt) with + Sys.Signal_handle f -> old_callback := f + | Sys.Signal_ignore + | Sys.Signal_default -> assert false + in + fun () -> + match !worker_thread with + None -> assert false + | Some t -> interrupt := Some (Thread.id t) in let keep_focus f = fun () -> try @@ -486,10 +808,19 @@ class gui () = match get_devel_selected () with | None -> () | Some d -> - let clean = locker - (fun () -> MatitamakeLib.publish_development_in_bg refresh d) - in - ignore(clean ()))); + let publish = locker (fun () -> + MatitamakeLib.publish_development_in_bg refresh d) in + ignore(publish ()))); + connect_button develList#graphButton (fun () -> + match get_devel_selected () with + | None -> () + | Some d -> + (match MatitamakeLib.dot_for_development d with + | None -> () + | Some _ -> + let browser = MatitaMathView.cicBrowser () in + browser#load (`Development + (MatitamakeLib.name_for_development d)))); connect_button develList#closeButton (fun () -> develList#toplevel#misc#hide()); ignore(develList#toplevel#event#connect#delete @@ -612,7 +943,7 @@ class gui () = (tac_w_term (A.Transitivity (loc, hole))); connect_button tbar#assumptionButton (tac (A.Assumption loc)); connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole))); - connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None))); + connect_button tbar#autoButton (tac (A.Auto (loc,[]))); MatitaGtkMisc.toggle_widget_visibility ~widget:(main#tacticsButtonsHandlebox :> GObj.widget) ~check:main#tacticsBarMenuItem; @@ -634,35 +965,7 @@ class gui () = | MatitaScript.ActionCancelled s -> HLog.error s | exn -> if not (Helm_registry.get_bool "matita.debug") then - let floc, msg = MatitaExcPp.to_string exn in - begin - match floc with - None -> () - | Some floc -> - let (x, y) = HExtlib.loc_of_floc floc in - let script = MatitaScript.current () in - let locked_mark = script#locked_mark in - let error_tag = script#error_tag in - let baseoffset = - (source_buffer#get_iter_at_mark (`MARK locked_mark))#offset in - let x' = baseoffset + x in - let y' = baseoffset + y in - let x_iter = source_buffer#get_iter (`OFFSET x') in - let y_iter = source_buffer#get_iter (`OFFSET y') in - source_buffer#apply_tag error_tag ~start:x_iter ~stop:y_iter; - let id = ref None in - id := Some (source_buffer#connect#changed ~callback:(fun () -> - source_buffer#remove_tag error_tag - ~start:source_buffer#start_iter - ~stop:source_buffer#end_iter; - match !id with - | None -> assert false (* a race condition occurred *) - | Some id -> - (new GObj.gobject_ops source_buffer#as_buffer)#disconnect id)); - source_buffer#place_cursor - (source_buffer#get_iter (`OFFSET x')); - end; - HLog.error msg + notify_exn exn else raise exn); (* script *) ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- [])); @@ -789,6 +1092,7 @@ class gui () = connect_button main#scriptTopButton top; connect_button main#scriptBottomButton bottom; connect_button main#scriptJumpButton jump; + connect_button main#scriptAbortButton kill_worker; connect_menu_item main#scriptAdvanceMenuItem advance; connect_menu_item main#scriptRetractMenuItem retract; connect_menu_item main#scriptTopMenuItem top; @@ -903,7 +1207,7 @@ class gui () = source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s in let get_ligature word = - let len = MatitaGtkMisc.utf8_string_length word in + let len = String.length word in let aux_tex () = try for i = len - 1 downto 0 do @@ -1007,16 +1311,34 @@ class gui () = method loadScript file = let script = MatitaScript.current () in script#reset (); - script#assignFileName file; - let content = - if Sys.file_exists file then file - else BuildTimeConf.script_template - in - source_view#source_buffer#begin_not_undoable_action (); - script#loadFromFile content; - source_view#source_buffer#end_not_undoable_action (); - console#message ("'"^file^"' loaded."); - self#_enableSaveTo file + if Pcre.pmatch ~pat:"\\.p$" file then + begin + let tptppath = + Helm_registry.get_opt_default Helm_registry.string ~default:"./" + "matita.tptppath" + in + let data = Matitaprover.p_to_ma ~filename:file ~tptppath () in + let filename = Pcre.replace ~pat:"\\.p$" ~templ:".ma" file in + script#assignFileName filename; + source_view#source_buffer#begin_not_undoable_action (); + script#loadFromString data; + source_view#source_buffer#end_not_undoable_action (); + console#message ("'"^filename^"' loaded."); + self#_enableSaveTo filename + end + else + begin + script#assignFileName file; + let content = + if Sys.file_exists file then file + else BuildTimeConf.script_template + in + source_view#source_buffer#begin_not_undoable_action (); + script#loadFromFile content; + source_view#source_buffer#end_not_undoable_action (); + console#message ("'"^file^"' loaded."); + self#_enableSaveTo file + end method setStar name b = let l = main#scriptLabel in @@ -1055,11 +1377,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 (); @@ -1264,36 +1581,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 =