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
(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;
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