diff options
Diffstat (limited to 'ide/session.ml')
| -rw-r--r-- | ide/session.ml | 37 |
1 files changed, 18 insertions, 19 deletions
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 ) |