since there is no more tab, the modification of the current file is in the window...

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 95d0a76310ebea5d645935ee81ea0b1914791ad7..f849dc25f5b5e84d09e067dd759687da415a0918 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -783,7 +783,9 @@ class gui () =
               notify_exn exc;
               unlock_world ()
        in
-        worker_thread := Some (Thread.create thread_main ()) in
+       (*thread_main ();*)
+       worker_thread := Some (Thread.create thread_main ())
+      in
       let kill_worker =
        (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *)
        let interrupt = ref None in
@@ -889,6 +891,8 @@ class gui () =
         | None -> true
         | Some path -> 
             let is_prefix_of d1 d2 =
+              let d1 = MatitamakeLib.normalize_path d1 in
+              let d2 = MatitamakeLib.normalize_path d2 in
               let len1 = String.length d1 in
               let len2 = String.length d2 in
               if len2 < len1 then 
@@ -960,59 +964,13 @@ class gui () =
         ignore (adj#connect#changed
                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
-        (* toolbar *)
-      let module A = GrafiteAst in
-      let hole = CicNotationPt.UserInput in
-      let loc = HExtlib.dummy_floc in
-      let tac ast _ =
-        if (MatitaScript.current ())#onGoingProof () then
-          (MatitaScript.current ())#advance
-            ~statement:("\n"
-              ^ GrafiteAstPp.pp_tactic
-                ~map_unicode_to_tex:(Helm_registry.get_bool
-                  "matita.paste_unicode_as_tex")
-                ~term_pp:CicNotationPp.pp_term
-                ~lazy_term_pp:CicNotationPp.pp_term ast)
-            ()
-      in
-      let tac_w_term ast _ =
-        if (MatitaScript.current ())#onGoingProof () then
-          let buf = source_buffer in
-          buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
-            ("\n"
-            ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
-              ~map_unicode_to_tex:(Helm_registry.get_bool
-                "matita.paste_unicode_as_tex")
-              ~lazy_term_pp:CicNotationPp.pp_term ast)
-      in
-      let tbar = main in
-      connect_button tbar#introsButton (tac (A.Intros (loc, (None, []))));
-      connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
-      connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
-      connect_button tbar#elimButton (tac_w_term
-        (let pattern = None, [], Some CicNotationPt.UserInput in
-       A.Elim (loc, hole, None, pattern, (None, []))));
-      connect_button tbar#elimTypeButton (tac_w_term
-        (A.ElimType (loc, hole, None, (None, []))));
-      connect_button tbar#splitButton (tac (A.Split loc));
-      connect_button tbar#leftButton (tac (A.Left loc));
-      connect_button tbar#rightButton (tac (A.Right loc));
-      connect_button tbar#existsButton (tac (A.Exists loc));
-      connect_button tbar#reflexivityButton (tac (A.Reflexivity loc));
-      connect_button tbar#symmetryButton (tac (A.Symmetry loc));
-      connect_button tbar#transitivityButton
-        (tac_w_term (A.Transitivity (loc, hole)));
-      connect_button tbar#assumptionButton (tac (A.Assumption loc));
-      connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.AutoBatch (loc,[])));
-      MatitaGtkMisc.toggle_widget_visibility
-       ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
-       ~check:main#tacticsBarMenuItem;
+      (* TO BE REMOVED *)
+      main#tacticsButtonsHandlebox#misc#hide ();
+      main#tacticsBarMenuItem#misc#hide ();
+      main#scriptNotebook#remove_page 1;
+      main#scriptNotebook#set_show_tabs false;
+      (* / TO BE REMOVED *)
       let module Hr = Helm_registry in
-      if
-        not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
-      then 
-        main#tacticsBarMenuItem#set_active false;
       MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
         ~callback:(function 
           | true -> main#toplevel#fullscreen () 
@@ -1030,8 +988,6 @@ class gui () =
       MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
         ~callback:(fun enabled ->
           Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
-      if not (Helm_registry.has "matita.paste_unicode_as_tex") then
-        Helm_registry.set_bool "matita.paste_unicode_as_tex" false;
       main#unicodeAsTexMenuItem#set_active
         (Helm_registry.get_bool "matita.paste_unicode_as_tex");
         (* log *)
@@ -1423,11 +1379,13 @@ class gui () =
         end
       
     method setStar name b =
-      let l = main#scriptLabel in
+      let w = main#toplevel in
+      let set x = w#set_title x in
+      let name = "Matita - " ^ name in
       if b then
-        l#set_text (name ^  " *")
+        set (name ^  " *")
       else
-        l#set_text (name)
+        set (name)
         
     method private _enableSaveTo file =
       script_fname <- Some file;