let clean_current_baseuri grafite_status =
LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status]
-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 no_pstatus =
GrafiteMarshal.save_moo moo_fname
grafite_status.GrafiteTypes.moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname
- lexicon_status.LexiconEngine.lexicon_content_rev
+ (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev
| _ -> clean_current_baseuri grafite_status
;;
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;