Source language and style are preferences

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15267 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 40 insertions, 44 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index b42651bdc7..429c4c334f 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1229,38 +1229,6 @@ object(self)
 	      | Interface.Good _ -> ()
   end
 
-  method private electric_paren tag =
-    let oparen_code = Glib.Utf8.to_unichar "("  ~pos:(ref 0) in
-    let cparen_code = Glib.Utf8.to_unichar ")"  ~pos:(ref 0) in
-    ignore (input_buffer#connect#insert_text ~callback:
-              (fun it x ->
-                input_buffer#remove_tag
-                  ~start:input_buffer#start_iter
-                  ~stop:input_buffer#end_iter
-                  tag;
-                if x = "" then () else
-                  match x.[String.length x - 1] with
-                    | ')' ->
-                      let hit = self#get_insert in
-                      let count = ref 0 in
-                      if hit#nocopy#backward_find_char
-                        (fun c ->
-                          if c = oparen_code && !count = 0 then true
-                          else if c = cparen_code then
-                            (incr count;false)
-                          else if c = oparen_code then
-                            (decr count;false)
-                          else false
-                        )
-                      then
-                        begin
-                          prerr_endline "Found matching parenthesis";
-                          input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char
-                        end
-                      else ()
-                    | _ -> ())
-  )
-
   method help_for_keyword () =
     browse_keyword (self#insert_message) (get_current_word ())
 
@@ -1363,7 +1331,6 @@ object(self)
     ignore (input_buffer#add_selection_clipboard cb);
     ignore (proof_buffer#add_selection_clipboard cb);
     ignore (message_buffer#add_selection_clipboard cb);
-    self#electric_paren Tags.Script.paren;
     ignore (input_buffer#connect#after#mark_set
               ~callback:(fun it (m:Gtk.text_mark) ->
                 !set_location
@@ -1371,11 +1338,7 @@ object(self)
                      "Line: %5d Char: %3d" (self#get_insert#line + 1)
                      (self#get_insert#line_offset + 1));
                 match GtkText.Mark.get_name m  with
-                  | Some "insert" ->
-                    input_buffer#remove_tag
-                      ~start:input_buffer#start_iter
-                      ~stop:input_buffer#end_iter
-                      Tags.Script.paren;
+                  | Some "insert" -> ()
                   | Some s ->
                     prerr_endline (s^" moved")
                   | None -> () )
@@ -1417,7 +1380,15 @@ let search_next_error () =
 let create_session file =
   let script =
     Undo.undoable_view
-      ~source_buffer:(GSourceView2.source_buffer ~tag_table:Tags.Script.table ())
+      ~source_buffer:(GSourceView2.source_buffer
+			~tag_table:Tags.Script.table
+			~highlight_matching_brackets:true
+			?language:
+			  (Preferences.lang_manager#language !current.source_language)
+			?style_scheme:
+			  (Preferences.style_manager#style_scheme !current.source_style)
+			())
+      ~show_line_numbers:true
       ~wrap_mode:`NONE () in
   let proof =
     GText.view
diff --git a/ide/preferences.ml b/ide/preferences.ml
index d320dddab4..8606370b70 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -11,6 +11,12 @@ open Printf
 
 let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc"
 let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys"
+let lang_manager = GSourceView2.source_language_manager ~default:true
+let () = lang_manager#set_search_path
+  (Minilib.xdg_data_dirs@lang_manager#search_path)
+let style_manager = GSourceView2.source_style_scheme_manager ~default:true
+let () = style_manager#set_search_path
+  (Minilib.xdg_data_dirs@style_manager#search_path)
 
 let get_config_file name =
   let find_config dir = Sys.file_exists (Filename.concat dir name) in
@@ -84,6 +90,9 @@ type pref =
       mutable cmd_coqmakefile : string;
       mutable cmd_coqdoc : string;
 
+      mutable source_language : string;
+      mutable source_style : string;
+
       mutable global_auto_revert : bool;
       mutable global_auto_revert_delay : int;
 
@@ -151,6 +160,9 @@ let (current:pref ref) =
     auto_save_delay = 10000;
     auto_save_name = "#","#";
 
+    source_language = "vernac";
+    source_style = "classic";
+
     read_project = Ignore_args;
     project_file_name = "_CoqProject";
 
@@ -211,6 +223,8 @@ let save_pref () =
     add "cmd_make" [p.cmd_make] ++
     add "cmd_coqmakefile" [p.cmd_coqmakefile] ++
     add "cmd_coqdoc" [p.cmd_coqdoc] ++
+    add "source_language" [p.source_language] ++
+    add "source_style" [p.source_style] ++
     add "global_auto_revert" [string_of_bool p.global_auto_revert] ++
     add "global_auto_revert_delay"
       [string_of_int p.global_auto_revert_delay] ++
@@ -273,6 +287,8 @@ let load_pref () =
     set_hd "cmd_make" (fun v -> np.cmd_make <- v);
     set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v);
     set_hd "cmd_coqdoc" (fun v -> np.cmd_coqdoc <- v);
+    set_hd "source_language" (fun v -> np.source_language <- v);
+    set_hd "source_style" (fun v -> np.source_style <- v);
     set_bool "global_auto_revert" (fun v -> np.global_auto_revert <- v);
     set_int "global_auto_revert_delay"
       (fun v -> np.global_auto_revert_delay <- v);
@@ -531,6 +547,13 @@ let configure ?(apply=(fun () -> ())) () =
       )
       (string_of_inputenc !current.encoding)
   in
+
+  let source_style =
+    combo "Highlighting style"
+      ~f:(fun s -> !current.source_style <- s) ~new_allowed:false
+      style_manager#style_scheme_ids !current.source_style
+  in
+
   let read_project =
     combo
       "Project file options are"
@@ -671,7 +694,7 @@ let configure ?(apply=(fun () -> ())) () =
      Section("Files", Some `DIRECTORY,
 	     [global_auto_revert;global_auto_revert_delay;
 	      auto_save; auto_save_delay; (* auto_save_name*)
-	      encodings;
+	      encodings;source_style;
 	     ]);
      Section("Project", Some (`STOCK "gtk-page-setup"),
 	     [project_file_name;read_project;
diff --git a/ide/preferences.mli b/ide/preferences.mli
index b680c6f029..fae7ebd9ff 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+val lang_manager : GSourceView2.source_language_manager
+val style_manager : GSourceView2.source_style_scheme_manager
+
 type project_behavior = Ignore_args | Append_args | Subst_args
 type inputenc = Elocale | Eutf8 | Emanual of string
 
@@ -17,6 +20,9 @@ type pref =
       mutable cmd_coqmakefile : string;
       mutable cmd_coqdoc : string;
 
+      mutable source_language : string;
+      mutable source_style : string;
+
       mutable global_auto_revert : bool;
       mutable global_auto_revert_delay : int;
 
diff --git a/ide/tags.ml b/ide/tags.ml
index 73da20f217..db1549e78f 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -32,9 +32,7 @@ struct
   let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
   let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false]
   let folded = make_tag table ~name:"locked" [`EDITABLE false; `BACKGROUND "light grey"]
-  let paren = make_tag table ~name:"paren" [`BACKGROUND "purple"]
   let sentence = make_tag table ~name:"sentence" []
-  let replaced = make_tag table ~name:"replaced" [`BACKGROUND "green"]
 end
 module Proof =
 struct
diff --git a/ide/tags.mli b/ide/tags.mli
index 4dc0b9fc8e..5a5356193b 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -22,9 +22,7 @@ sig
   val found : GText.tag
   val hidden : GText.tag
   val folded : GText.tag
-  val paren : GText.tag
   val sentence : GText.tag
-  val replaced : GText.tag
 end
 
 module Proof :