aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-04-10 16:01:42 +0000
committerGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-04-10 16:01:42 +0000
commit0e6f7047c2459628750377ee14c9fe4267408789 (patch)
tree0cb73f2101e9c34df50e9c369fa74af2acee13f8 /ide
parent1cd82289f21445fbe09f5810a103f3c786f72b42 (diff)
coqide: bug highlight corrige
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3903 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide.ml7
-rw-r--r--ide/highlight.mll15
2 files changed, 16 insertions, 6 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ca9172d68..614e475b4 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1627,7 +1627,8 @@ let main files =
(* File/Rehighlight Menu *)
let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in
ignore (rehighlight_m#connect#activate
- (fun () -> Highlight.highlight_all
+ (fun () ->
+ Highlight.rehighlight_all
(get_current_view()).view#buffer));
(* File/Refresh Menu *)
@@ -2215,9 +2216,7 @@ let start () =
cb_ := Some (GtkBase.Clipboard.get Gdk.Atom.primary);
Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
`WARNING;`CRITICAL]
- (fun ~level msg ->
- failwith ("Coqide internal error: " ^ msg)
- );
+ (fun ~level msg -> failwith ("Coqide internal error: " ^ msg));
Command_windows.main ();
main files;
while true do
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 2e8ce6659..a3af358a8 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -98,8 +98,8 @@ and comment = parse
try
let i = get_insert input_buffer in
highlight_slice input_buffer
- (i#backward_lines 3)
- (ignore (i#nocopy#forward_lines 3);i)
+ (i#backward_lines 10)
+ (ignore (i#nocopy#forward_lines 10);i)
with _ -> ()
@@ -108,4 +108,15 @@ and comment = parse
highlight_slice input_buffer input_buffer#start_iter input_buffer#end_iter
with _ -> ()
+ let rehighlight_all (input_buffer:GText.buffer) =
+ input_buffer#remove_tag_by_name
+ ~start:input_buffer#start_iter
+ ~stop:input_buffer#end_iter "kwd";
+ input_buffer#remove_tag_by_name
+ ~start:input_buffer#start_iter
+ ~stop:input_buffer#end_iter "decl";
+ input_buffer#remove_tag_by_name
+ ~start:input_buffer#start_iter
+ ~stop:input_buffer#end_iter "error";
+ highlight_all input_buffer
}