integrated lablgtksourceview

diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in
index 1715dd1f4352c90f034cf1c6298ffdd8a9d061cc..6b35fda1f04b843a420a2b668784aa82c88bde42 100644 (file)
--- a/helm/matita/buildTimeConf.ml.in
+++ b/helm/matita/buildTimeConf.ml.in
@@ -34,5 +34,9 @@ let phrase_sep = ".";;
 let blank_uri = "about:blank";;
 let current_proof_uri = "about:current_proof";;
 let default_script_font = "Monospace 10";;
-let images_dir = "@IMAGES_DIR@";;
+let runtime_base_dir = "@RT_BASE_DIR@";;
+
+let images_dir = runtime_base_dir ^ "/icons"
+let gtkrc_file = runtime_base_dir ^ "/matita.gtkrc"
+let lang_file  = runtime_base_dir ^ "/matita.lang"
 

diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac
index e7cd49fadeb8face6be24744756e97a7e6864d0c..e25e1c65c1aa7e3e029ab0c0d676ded7477e87a4 100644 (file)
--- a/helm/matita/configure.ac
+++ b/helm/matita/configure.ac
@@ -42,6 +42,7 @@ FINDLIB_REQUIRES="\
 $FINDLIB_CREQUIRES \
 lablgtk2.glade \
 lablgtkmathview \
+lablgtksourceview \
 helm-xmldiff \
 "
 for r in $FINDLIB_REQUIRES
@@ -86,8 +87,7 @@ if test "$DEBUG" = "true"; then
   echo "debugging enabled"
 fi
 
-MATITA_GTKRC="matita.gtkrc"
-IMAGES_DIR="icons"
+RT_BASE_DIR="."
 
 AC_SUBST(CAMLP4O)
 AC_SUBST(DEBUG)
@@ -97,8 +97,7 @@ AC_SUBST(FINDLIB_CREQUIRES)
 AC_SUBST(HAVE_OCAMLOPT)
 AC_SUBST(LABLGLADECC)
 AC_SUBST(OCAMLFIND)
-AC_SUBST(MATITA_GTKRC)
-AC_SUBST(IMAGES_DIR)
+AC_SUBST(RT_BASE_DIR)
 
 AC_OUTPUT([
   buildTimeConf.ml

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index bea43910b80469455c525ff33e6796a493562793..d1a39dd9d38c10a65d400159df174a7480109005 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -1906,7 +1906,7 @@ Copyright (C) 2005,
                              <property name="enable_popup">False</property>
 
                              <child>
-                               <widget class="GtkScrolledWindow" id="scrolledwindow7">
+                               <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
                                  <property name="visible">True</property>
                                  <property name="can_focus">True</property>
                                  <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
@@ -1915,24 +1915,7 @@ Copyright (C) 2005,
                                  <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 
                                  <child>
-                                   <widget class="GtkTextView" id="scriptTextView">
-                                     <property name="border_width">2</property>
-                                     <property name="visible">True</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="editable">True</property>
-                                     <property name="overwrite">False</property>
-                                     <property name="accepts_tab">True</property>
-                                     <property name="justification">GTK_JUSTIFY_LEFT</property>
-                                     <property name="wrap_mode">GTK_WRAP_NONE</property>
-                                     <property name="cursor_visible">True</property>
-                                     <property name="pixels_above_lines">0</property>
-                                     <property name="pixels_below_lines">0</property>
-                                     <property name="pixels_inside_wrap">0</property>
-                                     <property name="left_margin">2</property>
-                                     <property name="right_margin">0</property>
-                                     <property name="indent">0</property>
-                                     <property name="text" translatable="yes"></property>
-                                   </widget>
+                                   <placeholder/>
                                  </child>
                                </widget>
                                <packing>

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 97595d1926004de1e8eb2e844b34affb9b9caf14..5433a898b417513c4354286af73ad7b5c26354b2 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -37,7 +37,7 @@ let _ =
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
   MatitaDb.clean_owner_environment ();
   MatitaDb.create_owner_environment ();
-  GtkMain.Rc.add_default_file BuildTimeConf.gtkrc;  (* loads gtk rc files *)
+  GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
   ignore (GMain.Main.init ());
 
   (* environment trust *)
@@ -60,7 +60,7 @@ let _ =
 
 let script =
   MatitaScript.script 
-    ~buffer:gui#main#scriptTextView#buffer
+    ~buffer:gui#sourceView#buffer
     ~init:(Lazy.force MatitaEngine.initial_status) 
     ~mathviewer:(MatitaMathView.mathViewer ())
     ~urichooser:(fun uris ->
@@ -69,7 +69,7 @@ let script =
         ~title:"Matita: URI chooser" 
         ~msg:"Select the URI" ~hide_uri_entry:true
         ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
-        ~copy_cb:(fun s -> gui#main#scriptTextView#buffer#insert ("\n"^s^"\n"))
+        ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
         () ~id:"boh?" uris
       with MatitaTypes.Cancel -> [])
     ()

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 899c4b41eb6d7f0da0f0f1474f46e18c5764d268..b6b3f5ea2fd6efa7bdda78ed3fd4f63850ddbd17 100644 (file)
--- 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
@@ -169,6 +179,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 +221,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 +232,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 +250,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 +279,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 +302,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

diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli
index 674f3702cec56241bfd6d10af607e2f0ef394dc6..42922140c090de3a7f73ca3b00bd3adf2ffcc719 100644 (file)
--- a/helm/matita/matitaGui.mli
+++ b/helm/matita/matitaGui.mli
@@ -54,6 +54,7 @@ object
 (*   method toolbar :      MatitaGeneratedGui.toolBarWin *)
 
   method console:       console
+  method sourceView:    GSourceView.source_view
 
     (** {2 Dialogs instantiation}
      * methods below create a new window on each invocation. You should