X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=de78194f0254f0592642d8b90ad40c3ccd183fde;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=931fb049a492d1befc65be17e7a65edd71ad4501;hpb=90f5cf2abe808c8343847e1e910918440fb27410;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 931fb049a..de78194f0 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -117,11 +117,16 @@ 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 None ctx menv subst (parsed_text,parsed_text_length,
+          status `XTNone ctx menv subst (parsed_text,parsed_text_length,
             NotationPt.Cast (t,NotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in
@@ -132,7 +137,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
       let s = NTactics.intros_tac ~names_ref [] script#status in
       let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
       let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
-      [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
+      [s, nl ^ "#" ^ String.concat " #" !names_ref], "", parsed_text_length
   | TA.NAutoInteractive (_loc, (None,a)) -> 
       let trace_ref = ref [] in
       let s = NnAuto.auto_tac ~params:(None,a) ~trace_ref script#status in
@@ -140,10 +145,14 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
         try List.assoc "depth" a
         with Not_found -> ""
       in
-      let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
+      let width = 
+        try List.assoc "width" a
+        with Not_found -> ""
+      in
+      let trace = "/"^(if int_of_string depth > 1 then depth ^ " width=" ^ width else "")^" by " in
       let thms = 
         match !trace_ref with
-        | [] -> "{}"
+        | [] -> ""
         | thms -> 
            String.concat ", "  
              (HExtlib.filter_map (function 
@@ -153,7 +162,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
       in
       let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
       let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
-      [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
+      [s, nl ^ trace ^ thms ^ "/"], "", parsed_text_length
   | TA.NAutoInteractive (_, (Some _,_)) -> assert false
 
 let rec eval_executable include_paths (buffer : GText.buffer)
@@ -771,7 +780,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
@@ -829,12 +841,12 @@ object (self)
   method private _saveToBackupFile () =
     if buffer#modified then
       begin
-        let f = self#filename in
+        let f = self#filename ^ "~" in
         let oc = open_out f in
         output_string oc (buffer#get_text ~start:buffer#start_iter
                             ~stop:buffer#end_iter ());
         close_out oc;
-        HLog.debug ("backup " ^ f ^ " saved")                    
+        HLog.debug ("backup " ^ f ^ " saved")
       end
   
   method private reset_buffer =