X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2FmatitaScript.ml;h=cb443ae469254510b4a3e5ee2b459f9761001a47;hb=56fb3c39cc9186ad2700b0ee8ca37f8d759c2376;hp=d86871963437efbac813b5e63b590f98573af5ff;hpb=f7da48c844105a52a705872dfa0d4104de010c82;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index d86871963..cb443ae46 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -117,8 +117,13 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
            if tl <> [] then
             HLog.warn
              "Many goals focused. Using the context of the first one\n";
-           let _, ctx, _ = NCicUtils.lookup_meta g menv in
-            ctx in
+           let ctx = try
+             let _, ctx, _ = NCicUtils.lookup_meta g menv in ctx
+             with NCicUtils.Meta_not_found _ -> 
+               HLog.warn "Current goal is closed. Using empty context.";
+               [ ]
+           in ctx
+      in
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
           status `XTNone ctx menv subst (parsed_text,parsed_text_length,
@@ -771,7 +776,10 @@ object (self)
       buffer#move_mark mark mark_position;
       source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
      end;
-    while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+    let time0 = Unix.gettimeofday () in
+    GtkThread.sync (fun () -> while Glib.Main.pending () do ignore(Glib.Main.iteration false); done) ();
+    let time1 = Unix.gettimeofday () in
+    HLog.debug ("... refresh done in " ^ string_of_float (time1 -. time0) ^ "s")
 
   method clean_dirty_lock =
     let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in