1 files changed, 16 insertions, 23 deletions

diff --git a/ide/session.ml b/ide/session.ml
index 34c533b8..fc6340d2 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -8,8 +8,6 @@
 
 open Preferences
 
-let prefs = Preferences.current
-
 (** A session is a script buffer + proof + messages,
     interacting with a coqtop, and a few other elements around *)
 
@@ -18,7 +16,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
-    method refresh_color : unit -> unit
+    method data : 'a
   end
 
 class type control =
@@ -50,8 +48,8 @@ let create_buffer () =
   let buffer = GSourceView2.source_buffer
     ~tag_table:Tags.Script.table
     ~highlight_matching_brackets:true
-    ?language:(lang_manager#language prefs.source_language)
-    ?style_scheme:(style_manager#style_scheme prefs.source_style)
+    ?language:(lang_manager#language source_language#get)
+    ?style_scheme:(style_manager#style_scheme source_style#get)
     ()
   in
   let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in
@@ -110,10 +108,10 @@ let set_buffer_handlers
     let id = ref 0 in
     fun () -> incr id; !id in
   let running_action = ref None in
-  let cancel_signal reason =
+  let cancel_signal ?(stop_emit=true) reason =
     Minilib.log ("user_action cancelled: "^reason);
     action_was_cancelled := true;
-    GtkSignal.stop_emit () in
+    if stop_emit then GtkSignal.stop_emit () in
   let del_mark () =
     try buffer#delete_mark (`NAME "target")
     with GText.No_such_mark _ -> () in
@@ -126,7 +124,7 @@ let set_buffer_handlers
       fun () -> (* If Coq is busy due to the current action, we don't cancel *)
         match !running_action with
         | Some aid when aid = action -> ()
-        | _ -> cancel_signal "Coq busy" in
+        | _ -> cancel_signal ~stop_emit:false "Coq busy" in
     Coq.try_grab coqtop action fallback in
   let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in
   let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in
@@ -197,12 +195,8 @@ let set_buffer_handlers
          to a point indicated by coq. *)
       if !no_coq_action_required then begin
         let start, stop = get_start (), get_stop () in
-        buffer#remove_tag Tags.Script.error ~start ~stop;
-        buffer#remove_tag Tags.Script.error_bg ~start ~stop;
-        buffer#remove_tag Tags.Script.tooltip ~start ~stop;
-        buffer#remove_tag Tags.Script.processed ~start ~stop;
-        buffer#remove_tag Tags.Script.to_process ~start ~stop;
-        buffer#remove_tag Tags.Script.incomplete ~start ~stop;
+	List.iter (fun tag -> buffer#remove_tag tag ~start ~stop)
+		  Tags.Script.ephemere;
         Sentence.tag_on_insert buffer
       end;
     end in
@@ -254,10 +248,9 @@ let make_table_widget ?sort cd cb =
       ~model:store ~packing:frame#add () in
   let () = data#set_headers_visible true in
   let () = data#set_headers_clickable true in
-  let refresh () =
-    let clr = Tags.color_of_string current.background_color in
-    data#misc#modify_base [`NORMAL, `COLOR clr]
-  in
+  let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in
+  let _ = background_color#connect#changed refresh in
+  let _ = data#misc#connect#realize (fun () -> refresh background_color#get) in
   let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
   let cols =
     List.map2 (fun (_,c) (_,n,v) ->
@@ -285,10 +278,10 @@ let make_table_widget ?sort cd cb =
     data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc)
   );
   let () = match sort with None -> () | Some (i, t) -> store#set_sort_column_id i t in
-  frame, (fun f -> f columns store), refresh
+  frame, (fun f -> f columns store)
 
 let create_errpage (script : Wg_ScriptView.script_view) : errpage =
-  let table, access, refresh =
+  let table, access =
     make_table_widget ~sort:(0, `ASCENDING)
       [`Int,"Line",true; `String,"Error message",true]
       (fun columns store tp vc ->
@@ -320,11 +313,11 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
           errs
       end
     method on_update ~callback:cb = callback := cb
-    method refresh_color () = refresh ()
+    method data = !last_update
   end
 
 let create_jobpage coqtop coqops : jobpage =
-  let table, access, refresh =
+  let table, access =
     make_table_widget ~sort:(0, `ASCENDING)
       [`String,"Worker",true; `String,"Job name",true]
       (fun columns store tp vc ->
@@ -360,7 +353,7 @@ let create_jobpage coqtop coqops : jobpage =
           jobs
       end
     method on_update ~callback:cb = callback := cb
-    method refresh_color () = refresh ()
+    method data = !last_update
   end
 
 let create_proof () =