From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 ide/session.ml | 37 ++++++++++++++++++-------------------
 1 file changed, 18 insertions(+), 19 deletions(-)

(limited to 'ide/session.ml')

diff --git a/ide/session.ml b/ide/session.ml
index fc6340d2..be2bfe06 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Preferences
@@ -31,7 +33,7 @@ type session = {
   buffer : GText.buffer;
   script : Wg_ScriptView.script_view;
   proof : Wg_ProofView.proof_view;
-  messages : Wg_MessageView.message_view;
+  messages : Wg_RoutedMessageViews.message_views_router;
   segment : Wg_Segment.segment;
   fileops : FileOps.ops;
   coqops : CoqOps.ops;
@@ -209,10 +211,7 @@ let set_buffer_handlers
   let mark_set_cb it m =
     debug_edit_zone ();
     let ins = get_insert () in
-    let line = ins#line + 1 in
-    let off = ins#line_offset + 1 in
-    let msg = Printf.sprintf "Line: %5d Char: %3d" line off in
-    let () = !Ideutils.set_location msg in
+    let () = Ideutils.display_location ins in
     match GtkText.Mark.get_name m with
     | Some "insert" -> ()
     | Some s -> Minilib.log (s^" moved")
@@ -249,8 +248,8 @@ let make_table_widget ?sort cd cb =
   let () = data#set_headers_visible true in
   let () = data#set_headers_clickable true 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 _ = background_color#connect#changed ~callback:refresh in
+  let _ = data#misc#connect#realize ~callback:(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) ->
@@ -308,8 +307,8 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
         !callback errs;
 	List.iter (fun (lno, msg) -> access (fun columns store ->
           let line = store#append () in
-          store#set line (find_int_col "Line" columns) lno;
-          store#set line (find_string_col "Error message" columns) msg))
+          store#set ~row:line ~column:(find_int_col "Line" columns) lno;
+          store#set ~row:line ~column:(find_string_col "Error message" columns) msg))
           errs
       end
     method on_update ~callback:cb = callback := cb
@@ -348,8 +347,8 @@ let create_jobpage coqtop coqops : jobpage =
               else false)
           else
             let line = store#append () in
-            store#set line column id;
-            store#set line (find_string_col "Job name" columns) job))
+            store#set ~row:line ~column id;
+            store#set ~row:line ~column:(find_string_col "Job name" columns) job))
           jobs
       end
     method on_update ~callback:cb = callback := cb
@@ -367,7 +366,7 @@ let create_proof () =
 let create_messages () =
   let messages = Wg_MessageView.message_view () in
   let _ = messages#misc#set_can_focus true in
-  messages
+  Wg_RoutedMessageViews.message_views ~route_0:messages
 
 let dummy_control : control =
   object
@@ -386,12 +385,12 @@ let create file coqtop_args =
   let proof = create_proof () in
   let messages = create_messages () in
   let segment = new Wg_Segment.segment () in
-  let command = new Wg_Command.command_window basename coqtop in
   let finder = new Wg_Find.finder basename (script :> GText.view) in
   let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
   let _ = fops#update_stats in
   let cops =
     new CoqOps.coqops script proof messages segment coqtop (fun () -> fops#filename) in
+  let command = new Wg_Command.command_window basename coqtop cops messages in
   let errpage = create_errpage script in
   let jobpage = create_jobpage coqtop cops in
   let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in
@@ -512,12 +511,12 @@ let build_layout (sn:session) =
   sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
   script_scroll#add sn.script#coerce;
   proof_scroll#add sn.proof#coerce;
-  let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce in
+  let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#default_route#coerce in
   let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
   let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in
   (** When a message is received, focus on the message pane *)
   let _ =
-    sn.messages#connect#pushed ~callback:(fun _ _ ->
+    sn.messages#default_route#connect#pushed ~callback:(fun _ _ ->
       let num = message_frame#page_num detach#coerce in
       if 0 <= num then message_frame#goto_page num
     )
-- 
cgit v1.2.3