end
let clean_current_baseuri grafite_status =
- LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status]
+ LibraryClean.clean_baseuris [grafite_status#baseuri]
-let save_moo lexicon_status grafite_status =
+let save_moo grafite_status =
let script = MatitaScript.current () in
- let baseuri = GrafiteTypes.get_baseuri grafite_status in
+ let baseuri = grafite_status#baseuri in
let no_pstatus =
- grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
+ grafite_status#proof_status = GrafiteTypes.No_proof
in
match script#bos, script#eos, no_pstatus with
| true, _, _ -> ()
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- GrafiteMarshal.save_moo moo_fname
- grafite_status.GrafiteTypes.moo_content_rev;
+ GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname
- lexicon_status.LexiconEngine.lexicon_content_rev
+ grafite_status#lstatus.LexiconEngine.lexicon_content_rev;
+ NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
+ grafite_status#dump
| _ -> clean_current_baseuri grafite_status
;;
else main#tacticsButtonsHandlebox#misc#hide ())
~check:main#menuitemPalette;
connect_button main#butImpl_intro
- (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n");
+ (fun () -> source_buffer#insert "apply rule (⇒#i […] (…));\n");
connect_button main#butAnd_intro
(fun () -> source_buffer#insert
- "apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (∧#i (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butOr_intro_left
- (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∨#i_l (…));\n");
connect_button main#butOr_intro_right
- (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∨#i_r (…));\n");
connect_button main#butNot_intro
- (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n");
+ (fun () -> source_buffer#insert "apply rule (¬#i […] (…));\n");
connect_button main#butTop_intro
- (fun () -> source_buffer#insert "apply rule (⊤_i);\n");
+ (fun () -> source_buffer#insert "apply rule (⊤#i);\n");
connect_button main#butImpl_elim
(fun () -> source_buffer#insert
- "apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (⇒#e (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butAnd_elim_left
- (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∧#e_l (…));\n");
connect_button main#butAnd_elim_right
- (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∧#e_r (…));\n");
connect_button main#butOr_elim
(fun () -> source_buffer#insert
- "apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
+ "apply rule (∨#e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
connect_button main#butNot_elim
(fun () -> source_buffer#insert
- "apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (¬#e (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butBot_elim
- (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
+ (fun () -> source_buffer#insert "apply rule (⊥#e (…));\n");
connect_button main#butRAA
(fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
connect_button main#butUseLemma
(fun () -> source_buffer#insert "apply rule (discharge […]);\n");
connect_button main#butForall_intro
- (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∀#i {…} (…));\n");
connect_button main#butForall_elim
- (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∀#e {…} (…));\n");
connect_button main#butExists_intro
- (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∃#i {…} (…));\n");
connect_button main#butExists_elim
(fun () -> source_buffer#insert
- "apply rule (∃_e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
(* TO BE REMOVED *)
else saveAsScript ()
in
let abandon_script () =
- let lexicon_status = (s ())#lexicon_status in
let grafite_status = (s ())#grafite_status in
if source_view#buffer#modified then
(match ask_unsaved main#toplevel with
| `YES -> saveScript ()
| `NO -> ()
| `CANCEL -> raise MatitaTypes.Cancel);
- save_moo lexicon_status grafite_status
+ save_moo grafite_status
in
let loadScript () =
let script = s () in
match ask_unsaved main#toplevel with
| `YES ->
saveScript ();
- save_moo script#lexicon_status script#grafite_status;
+ save_moo script#grafite_status;
GMain.Main.quit ()
| `NO -> GMain.Main.quit ()
| `CANCEL -> ()
else
- (save_moo script#lexicon_status script#grafite_status;
+ (save_moo script#grafite_status;
GMain.Main.quit ()));
connect_button main#scriptAdvanceButton advance;
connect_button main#scriptRetractButton retract;