X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGui.ml;h=0ecede6227638f2a6dd304c35704491395d9617a;hb=76a993b80bb33d1075f84c55637ca1897644b16a;hp=cb7c63bac3ab49aa0d01caf02597a9578cdf3ba9;hpb=90f0070a8b639b622501bfff36e3e44853f34042;p=helm.git

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index cb7c63bac..0ecede622 100644
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -128,15 +128,19 @@ class console ~(buffer: GText.buffer) () =
 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 =
@@ -415,6 +419,7 @@ class gui () =
     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
@@ -769,7 +774,7 @@ class gui () =
       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
@@ -867,6 +872,9 @@ class gui () =
         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))