let clean_current_baseuri status =
LibraryClean.clean_baseuris [status#baseuri]
-let save_moo status =
- let script = MatitaScript.current () in
+let save_moo0 ~do_clean script status =
let baseuri = status#baseuri in
match script#bos, script#eos with
| true, _ -> ()
| _, true ->
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
status
- | _ -> clean_current_baseuri status
+ | _ -> if do_clean then clean_current_baseuri status
+;;
+
+let save_moo status =
+ let script = MatitaScript.current () in
+ save_moo0 ~do_clean:true script status
;;
let ask_unsaved parent filename =
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
+ val mutable current_page = 0
initializer
let s () = MatitaScript.current () in
main#unicodeAsTexMenuItem#set_active
(Helm_registry.get_bool "matita.paste_unicode_as_tex");
(* log *)
- HLog.set_log_callback self#console#log_callback;
+ HLog.set_log_callback (fun tag msg -> GtkThread.async (self#console#log_callback tag) msg);
GtkSignal.user_handler :=
(function
| MatitaScript.ActionCancelled s -> HLog.error s
MatitaMisc.reset_font_size;
ignore (main#scriptNotebook#connect#switch_page
(fun page ->
+ let old_script = MatitaScript.at_page current_page in
+ save_moo0 ~do_clean:false old_script old_script#status;
+ current_page <- page;
let script = MatitaScript.at_page page in
script#activate;
main#saveMenuItem#misc#set_sensitive script#has_name))