- bug fixed (introduced by last commit from Andrea in MatitaEngine):

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

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index d04fbcadab4b8bcace82958733d197b007742cc4..a0d731377cf65e6461963f654bf88801c41d948b 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -72,12 +72,9 @@ let clean_current_baseuri grafite_status =
 let save_moo grafite_status = 
   let script = MatitaScript.current () in
   let baseuri = grafite_status#baseuri in
-  let no_pstatus = 
-    grafite_status#proof_status = GrafiteTypes.No_proof 
-  in
-  match script#bos, script#eos, no_pstatus with
-  | true, _, _ -> ()
-  | _, true, true ->
+  match script#bos, script#eos with
+  | true, _ -> ()
+  | _, true ->
      let moo_fname = 
        LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
         ~writable:true in
@@ -870,7 +867,7 @@ class gui () =
           | false ->
               CicNotation.set_active_notations []);
       MatitaGtkMisc.toggle_callback ~check:main#hideCoercionsMenuItem
-        ~callback:(fun enabled -> Acic2content.hide_coercions := enabled);
+        ~callback:(fun enabled -> NTermCicContent.hide_coercions := enabled);
       MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
         ~callback:(fun enabled ->
           Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
@@ -887,18 +884,8 @@ class gui () =
           else raise exn);
         (* script *)
       let _ =
-        let source_language_manager =
-         GSourceView2.source_language_manager ~default:true in
-        source_language_manager#set_search_path
-         (BuildTimeConf.runtime_base_dir ::
-           source_language_manager#search_path);
-        match source_language_manager#language "grafite" with
-        | None ->
-            HLog.warn(sprintf "can't load a language file for \"grafite\" in %s"
-              BuildTimeConf.runtime_base_dir)
-        | Some x as matita_lang ->
-            source_buffer#set_language matita_lang;
-            source_buffer#set_highlight_syntax true
+       source_buffer#set_language (Some MatitaGtkMisc.matita_lang);
+       source_buffer#set_highlight_syntax true
       in
       let disableSave () =
         (s())#assignFileName None;
@@ -1008,8 +995,6 @@ class gui () =
         (fun _ -> 
           let c = MatitaMathView.cicBrowser () in
           c#load (`About `Hints));
-      connect_menu_item main#showAutoGuiMenuItem 
-        (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
       connect_menu_item main#showTermGrammarMenuItem 
         (fun _ -> 
           let c = MatitaMathView.cicBrowser () in
@@ -1379,8 +1364,7 @@ class gui () =
 
     method private updateFontSize () =
       self#sourceView#misc#modify_font_by_name
-        (sprintf "%s %d" BuildTimeConf.script_font font_size);
-      MatitaAutoGui.set_font_size font_size
+        (sprintf "%s %d" BuildTimeConf.script_font font_size)
 
     method increaseFontSize () =
       font_size <- font_size + 1;
@@ -1659,6 +1643,5 @@ let _ =
   Disambiguate.set_choose_interp_callback (interactive_interp_choice ());
   (* gtk initialization *)
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
-  GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
   ignore (GMain.Main.init ())