X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGui.ml;h=2a607d9fcf0cac59bf7a538d90b82c8239700952;hb=a5ba8bfcd6ae3b5033e58792092924455cc51837;hp=34406a3cd147908ef96d76a9804ecafc3064815f;hpb=7906a230a7989fab555d50ae930bb4169cb5d631;p=helm.git diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 34406a3cd..2a607d9fc 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -66,50 +66,59 @@ class console ~(buffer: GText.buffer) () = let clean_current_baseuri grafite_status = try let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in - let basedir = Helm_registry.get "matita.basedir" in - LibraryClean.clean_baseuris ~basedir [baseuri] + LibraryClean.clean_baseuris [baseuri] with GrafiteTypes.Option_error _ -> () let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = - let basedir = Helm_registry.get "matita.basedir" in - let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in - let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in - let save () = - let metadata_fname = - LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in - let lexicon_fname = - LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri - in - GrafiteMarshal.save_moo moo_fname - grafite_status.GrafiteTypes.moo_content_rev; - LibraryNoDb.save_metadata metadata_fname - lexicon_status.LexiconEngine.metadata; - LexiconMarshal.save_lexicon lexicon_fname - lexicon_status.LexiconEngine.lexicon_content_rev + let baseuri = + try Some (GrafiteTypes.get_string_option grafite_status "baseuri") + with GrafiteTypes.Option_error _ -> None in if (MatitaScript.current ())#eos && - grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof + grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof && + baseuri <> None then - begin - let rc = - MatitaGtkMisc.ask_confirmation - ~title:"A .moo can be generated" - ~message:(Printf.sprintf - "%s can be generated for %s.\nShould I generate it?" - (Filename.basename moo_fname) (Filename.basename fname)) - ~parent () - in - let b = - match rc with - | `YES -> true - | `NO -> false - | `CANCEL -> raise MatitaTypes.Cancel + begin + let baseuri = match baseuri with Some b -> b | None -> assert false in + let moo_fname = + LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri + ~writable:true in + let save () = + let metadata_fname = + LibraryMisc.metadata_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true in + let lexicon_fname = + LibraryMisc.lexicon_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true in - if b then - save () - else - clean_current_baseuri grafite_status - end + GrafiteMarshal.save_moo moo_fname + grafite_status.GrafiteTypes.moo_content_rev; + LibraryNoDb.save_metadata metadata_fname + lexicon_status.LexiconEngine.metadata; + LexiconMarshal.save_lexicon lexicon_fname + lexicon_status.LexiconEngine.lexicon_content_rev + in + begin + let rc = + MatitaGtkMisc.ask_confirmation + ~title:"A .moo can be generated" + ~message:(Printf.sprintf + "%s can be generated for %s.\nShould I generate it?" + (Filename.basename moo_fname) (Filename.basename fname)) + ~parent () + in + let b = + match rc with + | `YES -> true + | `NO -> false + | `CANCEL -> raise MatitaTypes.Cancel + in + if b then + save () + else + clean_current_baseuri grafite_status + end + end else clean_current_baseuri grafite_status @@ -206,6 +215,11 @@ class gui () = ~website:"http://helm.cs.unibo.it" () in + connect_menu_item main#contentsMenuItem (fun () -> + let cmd = + sprintf "gnome-help ghelp://%s/C/matita.xml &" BuildTimeConf.help_dir + in + ignore (Sys.command cmd)); connect_menu_item main#aboutMenuItem about_dialog#present; (* findRepl win *) let show_find_Repl () = @@ -401,17 +415,77 @@ 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; + main#scriptMenu#misc#set_sensitive true; source_view#set_editable true 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 exc -> + unlock_world (); + notify_exn exc + 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 @@ -467,6 +541,24 @@ class gui () = (fun () -> MatitamakeLib.clean_development_in_bg refresh d) in ignore(clean ()))); + connect_button develList#publishButton + (locker (fun () -> + match get_devel_selected () with + | None -> () + | Some d -> + 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 @@ -589,7 +681,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; @@ -608,38 +700,10 @@ class gui () = HLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := (function - | MatitaScript.ActionCancelled -> () + | 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 <- [])); @@ -766,6 +830,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; @@ -875,6 +940,7 @@ class gui () = method private nextLigature () = let iter = source_buffer#get_iter_at_mark `INSERT in let write_ligature len s = + assert(Glib.Utf8.validate s); source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len); source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s in @@ -918,7 +984,7 @@ class gui () = (match CicNotationLexer.lookup_ligatures ligature with | [] -> () | hd :: tl -> - write_ligature (String.length ligature) hd; + write_ligature (MatitaGtkMisc.utf8_string_length ligature) hd; next_ligatures <- tl @ [ hd ]) | hd :: tl -> write_ligature 1 hd; @@ -983,16 +1049,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 @@ -1240,7 +1324,8 @@ class interpModel = tree_store#get ~row:iter ~column:interp_no_col end -let interactive_interp_choice () choices = +let interactive_interp_choice () = + fun text prefix_len choices -> let gui = instance () in assert (choices <> []); let dialog = gui#newRecordDialog () in @@ -1269,6 +1354,127 @@ let interactive_interp_choice () choices = GtkThread.main (); (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel) +let interactive_string_choice + text prefix_len ?(title = "") ?(msg = "") () ~id locs uris += + let gui = instance () in + let dialog = gui#newUriDialog () in + dialog#uriEntryHBox#misc#hide (); + dialog#uriChoiceSelectedButton#misc#hide (); + dialog#uriChoiceAutoButton#misc#hide (); + dialog#uriChoiceConstantsButton#misc#hide (); + dialog#uriChoiceTreeView#selection#set_mode + (`SINGLE :> Gtk.Tags.selection_mode); + let model = new stringListModel dialog#uriChoiceTreeView in + let choices = ref None in + dialog#uriChoiceDialog#set_title title; + let hack_len = MatitaGtkMisc.utf8_string_length text in + let rec colorize acc_len = function + | [] -> + let floc = HExtlib.floc_of_loc (acc_len,hack_len) in + fst(MatitaGtkMisc.utf8_parsed_text text floc) + | he::tl -> + let start, stop = HExtlib.loc_of_floc he in + let floc1 = HExtlib.floc_of_loc (acc_len,start) in + let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in + let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in + str1 ^ "" ^ str2 ^ "" ^ colorize stop tl + in +(* List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in + Printf.eprintf "(%d,%d)" start stop) locs; *) + let locs = + List.sort + (fun loc1 loc2 -> + fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2)) + locs + in +(* prerr_endline "XXXXXXXXXXXXXXXXXXXX"; + List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in + Printf.eprintf "(%d,%d)" start stop) locs; + prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *) + dialog#uriChoiceLabel#set_use_markup true; + let txt = colorize 0 locs in + let txt,_ = MatitaGtkMisc.utf8_parsed_text txt + (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt)) + in + dialog#uriChoiceLabel#set_label txt; + List.iter model#easy_append uris; + let return v = + choices := v; + dialog#uriChoiceDialog#destroy (); + GMain.Main.quit () + in + ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); + connect_button dialog#uriChoiceForwardButton (fun _ -> + match model#easy_selection () with + | [] -> () + | uris -> return (Some uris)); + connect_button dialog#uriChoiceAbortButton (fun _ -> return None); + dialog#uriChoiceDialog#show (); + GtkThread.main (); + (match !choices with + | None -> raise MatitaTypes.Cancel + | Some uris -> uris) + +let interactive_interp_choice () text prefix_len choices = +(* List.iter (fun (l,_,_) -> + List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in + Printf.eprintf "(%d,%d)" start stop) l; prerr_endline "") + ((List.hd choices)); *) + let filter_choices filter = + let rec is_compatible filter = + function + [] -> true + | (_,id,dsc)::tl -> + try + if List.assoc id filter = dsc then + is_compatible filter tl + else + false + with + Not_found -> true + in + List.filter (fun (_,interp) -> is_compatible filter interp) + in + let rec get_choices id = + function + [] -> [] + | (_,he)::tl -> + let _,_,dsc = List.find (fun (_,id',_) -> id = id') he in + dsc :: (List.filter (fun dsc' -> dsc <> dsc') (get_choices id tl)) + in + let example_interp = + match choices with + [] -> assert false + | he::_ -> he in + let ask_user id locs choices = + interactive_string_choice + text prefix_len + ~title:"Ambiguous input" + ~msg:("Choose an interpretation for " ^ id) () ~id locs choices + in + let rec classify ids filter partial_interpretations = + match ids with + [] -> List.map fst partial_interpretations + | (locs,id,_)::tl -> + let choices = get_choices id partial_interpretations in + let chosen_dsc = + match choices with + [dsc] -> dsc + | _ -> + match ask_user id locs choices with + [x] -> x + | _ -> assert false + in + let filter = (id,chosen_dsc)::filter in + let compatible_interps = filter_choices filter partial_interpretations in + classify tl filter compatible_interps in + let enumerated_choices = + let idx = ref ~-1 in + List.map (fun interp -> incr idx; !idx,interp) choices + in + classify example_interp [] enumerated_choices + let _ = (* disambiguator callbacks *) GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ());