diff options
Diffstat (limited to 'ide/session.ml')
| -rw-r--r-- | ide/session.ml | 24 |
1 files changed, 19 insertions, 5 deletions
diff --git a/ide/session.ml b/ide/session.ml index 2936321128..dc79fa7905 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -133,6 +133,11 @@ let set_buffer_handlers try ignore(buffer#get_mark (`NAME "stop_of_input")) with GText.No_such_mark _ -> assert false in let get_insert () = buffer#get_iter_at_mark `INSERT in + let update_prev it = + let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in + if it#offset < prev#offset then + buffer#move_mark (`NAME "prev_insert") ~where:it + in let debug_edit_zone () = if false (*!Minilib.debug*) then begin buffer#remove_tag Tags.Script.edit_zone ~start:buffer#start_iter ~stop:buffer#end_iter; @@ -147,6 +152,7 @@ let set_buffer_handlers let insert_cb it s = if String.length s = 0 then () else begin Minilib.log ("insert_cb " ^ string_of_int it#offset); let text_mark = add_mark it in + let () = update_prev it in if it#has_tag Tags.Script.to_process then cancel_signal "Altering the script being processed in not implemented" else if it#has_tag Tags.Script.read_only then @@ -160,9 +166,9 @@ let set_buffer_handlers end end in let delete_cb ~start ~stop = Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset); - cur_action := new_action_id (); let min_iter, max_iter = if start#compare stop < 0 then start, stop else stop, start in + let () = update_prev min_iter in let text_mark = add_mark min_iter in let rec aux min_iter = if min_iter#equal max_iter then () @@ -465,7 +471,7 @@ let build_layout (sn:session) = message_frame#misc#show (); detachable#show); detachable#button#misc#hide (); - lbl in + detachable, lbl in let session_tab = GPack.hbox ~homogeneous:false () in let img = GMisc.image ~icon_size:`SMALL_TOOLBAR ~packing:session_tab#pack () in @@ -496,9 +502,17 @@ 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; - ignore(add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce); - let label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in - ignore(add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce); + let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#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 _ _ -> + let num = message_frame#page_num detach#coerce in + if 0 <= num then message_frame#goto_page num + ) + in + (** When an error occurs, paint the error label in red *) let txt = label#text in let red s = "<span foreground=\"#FF0000\">" ^ s ^ "</span>" in sn.errpage#on_update ~callback:(fun l -> |