hidded all hbugs related stuff

[helm.git] / matita / matitaGui.ml

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 8ffa5fc914e77f522f1b9849b1f19f1bfcda4268..01ced58a75217a426518898853f77669fd0594ef 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,54 +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 ~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
-              ~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 () 
@@ -1025,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 *)
@@ -1183,10 +1144,13 @@ class gui () =
       self#updateFontSize ();
         (* debug menu *)
       main#debugMenu#misc#hide ();
-        (* status bar *)
+        (* HBUGS *)
+      main#hintNotebook#misc#hide ();
+      (*
       main#hintLowImage#set_file (image_path "matita-bulb-low.png");
       main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
       main#hintHighImage#set_file (image_path "matita-bulb-high.png");
+      *)
         (* focus *)
       self#sourceView#misc#grab_focus ();
         (* main win dimension *)
@@ -1418,11 +1382,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;