On-going porting to lablgtk3

[helm.git] / matita / matita / matitaScript.ml

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index d86871963437efbac813b5e63b590f98573af5ff..33296d2320ec2be4487110090af548ba9586d86b 100644 (file)
--- 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,
@@ -140,7 +145,11 @@ 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
         | [] -> ""
@@ -242,7 +251,7 @@ let fresh_script_id =
  *)
 class script ~(parent:GBin.scrolled_window) ~tab_label () =
 let source_view =
-  GSourceView2.source_view
+  GSourceView3.source_view
     ~auto_indent:true
     ~insert_spaces_instead_of_tabs:true ~tab_width:2
     ~right_margin_position:80 ~show_right_margin:true
@@ -251,6 +260,12 @@ let source_view =
     () in
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
+let _ =
+ source_buffer#connect#notify_can_undo
+  ~callback:(MatitaMisc.get_gui ())#main#undoMenuItem#misc#set_sensitive in
+let _ =
+ source_buffer#connect#notify_can_redo
+  ~callback:(MatitaMisc.get_gui ())#main#redoMenuItem#misc#set_sensitive in
 let similarsymbols_tag_name = "similarsymbolos" in
 let similarsymbols_tag = `NAME similarsymbols_tag_name in
 let initial_statuses current baseuri =
@@ -367,16 +382,14 @@ object (self)
          | _ -> assert false in
        let add_menu_item =
          let i = ref 2 in (* last occupied position *)
-         fun ?label ?stock () ->
+         fun ~label ->
            incr i;
-           GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i)
-            ()
-       in
-       let copy = add_menu_item ~stock:`COPY () in
-       let cut = add_menu_item ~stock:`CUT () in
-       let delete = add_menu_item ~stock:`DELETE () in
-       let paste = add_menu_item ~stock:`PASTE () in
-       let paste_pattern = add_menu_item ~label:"Paste as pattern" () in
+           GMenu.menu_item ~label ~packing:(menu#insert ~pos:!i) () in
+       let copy = add_menu_item ~label:"Copy" in
+       let cut = add_menu_item ~label:"Cut" in
+       let delete = add_menu_item ~label:"Delete" in
+       let paste = add_menu_item ~label:"Paste" in
+       let paste_pattern = add_menu_item ~label:"Paste as pattern" in
        copy#misc#set_sensitive self#canCopy;
        cut#misc#set_sensitive self#canCut;
        delete#misc#set_sensitive self#canDelete;
@@ -388,24 +401,22 @@ object (self)
        MatitaGtkMisc.connect_menu_item paste self#paste;
        MatitaGtkMisc.connect_menu_item paste_pattern self#pastePattern;
        let new_undoMenuItem =
-        GMenu.image_menu_item
-         ~image:(GMisc.image ~stock:`UNDO ())
+        GMenu.menu_item
          ~use_mnemonic:true
          ~label:"_Undo"
          ~packing:(menu#insert ~pos:0) () in
        new_undoMenuItem#misc#set_sensitive
-        (undoMenuItem#misc#get_flag `SENSITIVE);
+        undoMenuItem#misc#sensitive;
        menu#remove (undoMenuItem :> GMenu.menu_item);
        MatitaGtkMisc.connect_menu_item new_undoMenuItem
         (fun () -> self#safe_undo);
        let new_redoMenuItem =
-        GMenu.image_menu_item
-         ~image:(GMisc.image ~stock:`REDO ())
+        GMenu.menu_item
          ~use_mnemonic:true
          ~label:"_Redo"
          ~packing:(menu#insert ~pos:1) () in
        new_redoMenuItem#misc#set_sensitive
-        (redoMenuItem#misc#get_flag `SENSITIVE);
+        redoMenuItem#misc#sensitive;
         menu#remove (redoMenuItem :> GMenu.menu_item);
         MatitaGtkMisc.connect_menu_item new_redoMenuItem
          (fun () -> self#safe_redo)));
@@ -771,7 +782,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