X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaGui.ml;h=c891a0bde63ec069fd9ec1207adde788589aa40a;hb=7fb4b063ed9488bbffa34d1cd193fca6c288a425;hp=899c4b41eb6d7f0da0f0f1474f46e18c5764d268;hpb=6e289c07138a9840beff4833b57521593fd732b1;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 899c4b41e..c891a0bde 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -68,6 +68,16 @@ class gui () =
     [ main#mainWinEventBox ]
   in
   let console = new console ~buffer:main#logTextView#buffer () in
+  let (source_view: GSourceView.source_view) =
+    GSourceView.source_view
+      ~auto_indent:true
+      ~insert_spaces_instead_of_tabs:true ~tabs_width:2
+      ~margin:80 ~show_margin:true
+      ~smart_home_end:true
+      ~packing:main#scriptScrolledWin#add
+      ()
+  in
+  let source_buffer = source_view#source_buffer in
   object (self)
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
@@ -133,7 +143,7 @@ class gui () =
       in
       let tac_w_term ast _ =
         if (MatitaScript.instance ())#onGoingProof () then
-          let (buf: GText.buffer) = self#main#scriptTextView#buffer in
+          let buf = source_buffer in
           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
             ("\n" ^ TacticAstPp.pp_tactic ast)
       in
@@ -160,6 +170,12 @@ class gui () =
       let module Hr = Helm_registry in
       if not(Hr.get_opt_default Hr.get_bool false "matita.tactics_bar") then 
         self#main#tacticsBarMenuItem#set_active false;
+      MatitaGtkMisc.toggle_callback 
+        ~callback:(function 
+          | true -> self#main#toplevel#fullscreen () 
+          | false -> self#main#toplevel#unfullscreen ())
+        ~check:self#main#fullscreenMenuItem;
+      self#main#fullscreenMenuItem#set_active false;
         (* quit *)
       self#setQuitCallback (fun () -> exit 0);
         (* log *)
@@ -169,6 +185,15 @@ class gui () =
            MatitaLog.error
              (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
         (* script *)
+      let _ =
+        match GSourceView.source_language_from_file BuildTimeConf.lang_file with
+        | None ->
+            MatitaLog.warn (sprintf "can't load language file %s"
+              BuildTimeConf.lang_file)
+        | Some matita_lang ->
+            source_buffer#set_language matita_lang;
+            source_buffer#set_highlight true
+      in
       let s () = MatitaScript.instance () in
       let disableSave () =
         script_fname <- None;
@@ -202,8 +227,8 @@ class gui () =
       in
       let newScript () = (s ())#reset (); disableSave () in
       let cursor () =
-        let buf = self#main#scriptTextView#buffer in
-        buf#place_cursor (buf#get_iter_at_mark (`NAME "locked"))
+        source_buffer#place_cursor
+          (source_buffer#get_iter_at_mark (`NAME "locked"))
       in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
@@ -213,7 +238,7 @@ class gui () =
       let connect_key sym f =
         connect_key self#main#mainWinEventBox#event
           ~modifiers:[`CONTROL] ~stop:true sym f;
-        connect_key self#main#scriptTextView#event
+        connect_key self#sourceView#event
           ~modifiers:[`CONTROL] ~stop:true sym f
       in
       connect_button self#main#scriptAdvanceButton advance;
@@ -231,27 +256,27 @@ class gui () =
       connect_menu_item self#main#newMenuItem    newScript;
       connect_key GdkKeysyms._period
         (fun () ->
-           let buf = self#main#scriptTextView#buffer in
-           buf#insert ~iter:(buf#get_iter_at_mark `INSERT) ".\n";
-           advance ());
+          source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
+            ".\n";
+          advance ());
       connect_key GdkKeysyms._Return
         (fun () ->
-           let buf = self#main#scriptTextView#buffer in
-           buf#insert ~iter:(buf#get_iter_at_mark `INSERT) "\n";
-           advance ());
+          source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
+            "\n";
+          advance ());
          (* script monospace font stuff *)  
       let font =
         Helm_registry.get_opt_default Helm_registry.get
           BuildTimeConf.default_script_font "matita.script_font"
       in
 (*       let monospace_tag = 
-        self#main#scriptTextView#buffer#create_tag [`FONT_DESC font] 
+        source_buffer#create_tag [`FONT_DESC font] 
       in *)
-      self#main#scriptTextView#misc#modify_font_by_name font;
+      self#sourceView#misc#modify_font_by_name font;
 (*       let _ = 
-        self#main#scriptTextView#buffer#connect#changed ~callback:(fun _ ->
-          let start, stop = self#main#scriptTextView#buffer#bounds in
-          self#main#scriptTextView#buffer#apply_tag monospace_tag start stop)
+        source_buffer#connect#changed ~callback:(fun _ ->
+          let start, stop = source_buffer#bounds in
+          source_buffer#apply_tag monospace_tag start stop)
       in *)
         (* debug menu *)
       self#main#debugMenu#misc#hide ();
@@ -260,7 +285,7 @@ class gui () =
       self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
       self#main#hintHighImage#set_file (image_path "matita-bulb-high.png");
         (* focus *)
-      self#main#scriptTextView#misc#grab_focus ();
+      self#sourceView#misc#grab_focus ();
         (* main win dimension *)
       let width = Gdk.Screen.width () in
       let height = Gdk.Screen.height () in
@@ -283,7 +308,7 @@ class gui () =
         
 
     method console = console
-
+    method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
     method about = about
     method fileSel = fileSel
     method main = main