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

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index cb7c63bac..ce3dcc6fe 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 = -1
       
     initializer
       let s () = MatitaScript.current () in
@@ -606,11 +611,15 @@ class gui () =
           let saved_use_library= !MultiPassDisambiguator.use_library in
           try
            MultiPassDisambiguator.use_library := !all_disambiguation_passes;
+           prerr_endline "PRIMA";
            f script;
            MultiPassDisambiguator.use_library := saved_use_library;
-           unlock_world ()
+           prerr_endline "DOPO";
+           unlock_world () ;
+           prerr_endline "FINE";
           with
            | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+              prerr_endline "EXC1";
               (try
                 interactive_error_interp 
                  ~all_passes:!all_disambiguation_passes source_view#source_buffer
@@ -627,7 +636,9 @@ class gui () =
                        notify_exn source_view exc);
                 | exc -> notify_exn source_view exc);
               MultiPassDisambiguator.use_library := saved_use_library;
-              unlock_world ()
+              prerr_endline "DOPO1";
+              unlock_world ();
+              prerr_endline "FINE1"
            | exc ->
               (try notify_exn source_view exc
                with Sys.Break as e -> notify_exn source_view e);
@@ -769,7 +780,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
@@ -865,11 +876,12 @@ class gui () =
         MatitaMisc.decrease_font_size;
       connect_menu_item main#normalFontSizeMenuItem
         MatitaMisc.reset_font_size;
-      ignore (main#scriptNotebook#connect#switch_page
-       (fun page ->
-         let script = MatitaScript.at_page page in
-          script#activate;
-          main#saveMenuItem#misc#set_sensitive script#has_name))
+      ignore (main#scriptNotebook#connect#switch_page (fun page ->
+        self#save_page ();
+        current_page <- page;
+        let script = MatitaScript.at_page page in
+        script#activate;
+        main#saveMenuItem#misc#set_sensitive script#has_name))
 
     method private externalEditor () =
      let script = MatitaScript.current () in
@@ -971,7 +983,13 @@ class gui () =
      let script = MatitaScript.at_page page in 
       self#closeScript page script
 
+    method private save_page () =
+      if current_page >= 0 then
+        let old_script = MatitaScript.at_page current_page in
+        save_moo0 ~do_clean:false old_script old_script#status
+
     method newScript () = 
+       self#save_page ();
        let scrolledWindow = GBin.scrolled_window () in
        let hbox = GPack.hbox () in
        let tab_label = GMisc.label ~text:"foo" ~packing:hbox#pack () in