with GrafiteTypes.Option_error _ -> ()
let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status =
- let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname 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
- 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.\n<i>Should I generate it?</i>"
- (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.\n<i>Should I generate it?</i>"
+ (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
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 ->
+ 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
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;
| 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 <- []));
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;
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
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
projects / helm.git / blobdiff