From 079e895cad0a205e22202da5ba1a919a820c863b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 8 Mar 2018 16:18:42 +0100 Subject: coqide: queries from the query window are routed there (fix #5684) We systematically use Wg_MessageView for both the message panel and each Query tab; we register all MessageView in a RoutedMessageViews where the default route (0) is the message panel. Queries from the Query panel pick a non zero route to have their feedback message delivered to their MessageView --- ide/coqOps.ml | 85 +++++++++++++++-------------------------- ide/coqOps.mli | 8 ++-- ide/coqide.ml | 89 ++++++++++++++++--------------------------- ide/ide.mllib | 3 +- ide/ideutils.ml | 12 ++++++ ide/ideutils.mli | 4 ++ ide/session.ml | 10 ++--- ide/session.mli | 2 +- ide/wg_Command.ml | 36 +++++++++-------- ide/wg_Command.mli | 2 +- ide/wg_MessageView.ml | 12 ++++-- ide/wg_MessageView.mli | 4 +- ide/wg_RoutedMessageViews.ml | 47 +++++++++++++++++++++++ ide/wg_RoutedMessageViews.mli | 23 +++++++++++ 14 files changed, 193 insertions(+), 144 deletions(-) create mode 100644 ide/wg_RoutedMessageViews.ml create mode 100644 ide/wg_RoutedMessageViews.mli (limited to 'ide') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index b45a87b1f..78fbce5c8 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -141,7 +141,8 @@ object method process_next_phrase : unit task method process_until_end_or_error : unit task method handle_reset_initial : unit task - method raw_coq_query : string -> unit task + method raw_coq_query : + route_id:int -> next:(query_rty value -> unit task) -> string -> unit task method show_goals : unit task method backtrack_last_phrase : unit task method initialize : unit task @@ -164,17 +165,6 @@ let flags_to_color f = else if List.mem `INCOMPLETE f then `NAME "gray" else `NAME Preferences.processed_color#get -(* Move to utils? *) -let rec validate (s : Pp.t) = match Pp.repr s with - | Pp.Ppcmd_empty - | Pp.Ppcmd_print_break _ - | Pp.Ppcmd_force_newline -> true - | Pp.Ppcmd_glue l -> List.for_all validate l - | Pp.Ppcmd_string s -> Glib.Utf8.validate s - | Pp.Ppcmd_box (_,s) - | Pp.Ppcmd_tag (_,s) -> validate s - | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s - module Doc = Document let segment_model (doc : sentence Doc.document) : Wg_Segment.model = @@ -229,7 +219,7 @@ end class coqops (_script:Wg_ScriptView.script_view) (_pv:Wg_ProofView.proof_view) - (_mv:Wg_MessageView.message_view) + (_mv:Wg_RoutedMessageViews.message_views_router) (_sg:Wg_Segment.segment) (_ct:Coq.coqtop) get_filename = @@ -364,23 +354,12 @@ object(self) method show_goals = self#show_goals_aux () (* This method is intended to perform stateless commands *) - method raw_coq_query phrase = + method raw_coq_query ~route_id ~next phrase : unit Coq.task = let sid = try Document.tip document with Document.Empty -> Stateid.initial in let action = log "raw_coq_query starting now" in - let display_error s = - if not (validate s) then - flash_info "This error is so nasty that I can't even display it." - else messages#add s; - in - let query = - let route_id = 0 in - Coq.query (route_id,(phrase,sid)) in - let next = function - | Fail (_, _, err) -> display_error err; Coq.return () - | Good msg -> Coq.return () - in + let query = Coq.query (route_id,(phrase,sid)) in Coq.bind (Coq.seq action query) next method private mark_as_needed sentence = @@ -472,22 +451,22 @@ object(self) self#mark_as_needed sentence; self#attach_tooltip ?loc sentence rmsg; self#position_tag_at_sentence ?loc Tags.Script.error sentence - | Message(Warning, loc, msg), Some (id,sentence) -> - log_pp ?id Pp.(str "WarningMsg " ++ msg); - let rmsg = Pp.string_of_ppcmds msg in + | Message(Warning, loc, message), Some (id,sentence) -> + log_pp ?id Pp.(str "WarningMsg " ++ message); + let rmsg = Pp.string_of_ppcmds message in add_flag sentence (`WARNING (loc, rmsg)); self#attach_tooltip ?loc sentence rmsg; self#position_tag_at_sentence ?loc Tags.Script.warning sentence; - messages#push Warning msg - | Message(lvl, loc, msg), Some (id,sentence) -> - log_pp ?id Pp.(str "Msg " ++ msg); - messages#push lvl msg + (messages#route msg.route)#push Warning message + | Message(lvl, loc, message), Some (id,sentence) -> + log_pp ?id Pp.(str "Msg " ++ message); + (messages#route msg.route)#push lvl message (* We do nothing here as for BZ#5583 *) | Message(Error, loc, msg), None -> log_pp Pp.(str "Error Msg without a sentence" ++ msg) - | Message(lvl, loc, msg), None -> - log_pp Pp.(str "Msg without a sentence " ++ msg); - messages#push lvl msg + | Message(lvl, loc, message), None -> + log_pp Pp.(str "Msg without a sentence " ++ message); + (messages#route msg.route)#push lvl message | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n @@ -538,8 +517,8 @@ object(self) if Stateid.equal id tip || Stateid.equal id Stateid.dummy then begin self#position_tag_at_iter ?loc start stop Tags.Script.error phrase; buffer#place_cursor ~where:stop; - messages#clear; - messages#push Feedback.Error msg; + messages#default_route#clear; + messages#default_route#push Feedback.Error msg; self#show_goals end else self#show_goals_aux ~move_insert:true () @@ -597,12 +576,12 @@ object(self) (** Compute the phrases until [until] returns [true]. *) method private process_until ?move_insert until verbose = - let logger lvl msg = if verbose then messages#push lvl msg in + let logger lvl msg = if verbose then messages#default_route#push lvl msg in let fill_queue = Coq.lift (fun () -> let queue = Queue.create () in (* Lock everything and fill the waiting queue *) push_info "Coq is computing"; - messages#clear; + messages#default_route#clear; script#set_editable false; self#fill_command_queue until queue; (* Now unlock and process asynchronously. Since [until] @@ -664,8 +643,9 @@ object(self) method join_document = let next = function | Good _ -> - messages#clear; - messages#push Feedback.Info (Pp.str "All proof terms checked by the kernel"); + messages#default_route#clear; + messages#default_route#push + Feedback.Info (Pp.str "All proof terms checked by the kernel"); Coq.return () | Fail x -> self#handle_failure x in Coq.bind (Coq.status true) next @@ -767,7 +747,7 @@ object(self) conclusion () | Fail (safe_id, loc, msg) -> (* if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); *) - messages#push Feedback.Error msg; + messages#default_route#push Feedback.Error msg; if Stateid.equal safe_id Stateid.dummy then self#show_goals else undo safe_id (Doc.focused document && Doc.is_in_focus document safe_id)) @@ -784,7 +764,7 @@ object(self) method private handle_failure_aux ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = - messages#push Feedback.Error msg; + messages#default_route#push Feedback.Error msg; ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) else @@ -796,7 +776,7 @@ object(self) method handle_failure f = self#handle_failure_aux f method backtrack_last_phrase = - messages#clear; + messages#default_route#clear; try let tgt = Doc.before_tip document in self#backtrack_to_id tgt @@ -804,7 +784,7 @@ object(self) method go_to_insert = Coq.bind (Coq.return ()) (fun () -> - messages#clear; + messages#default_route#clear; let point = self#get_insert in if point#compare self#get_start_of_input >= 0 then self#process_until_iter point @@ -812,7 +792,7 @@ object(self) method go_to_mark m = Coq.bind (Coq.return ()) (fun () -> - messages#clear; + messages#default_route#clear; let point = buffer#get_iter_at_mark m in if point#compare self#get_start_of_input >= 0 then Coq.seq (self#process_until_iter point) @@ -837,14 +817,11 @@ object(self) ~stop:(`MARK (buffer#create_mark stop)) [] in Doc.push document sentence; - messages#clear; + messages#default_route#clear; self#show_goals in let display_error (loc, s) = - if not (validate s) then - flash_info "This error is so nasty that I can't even display it." - else messages#add s - in + messages#default_route#add (Ideutils.validate s) in let try_phrase phrase stop more = let action = log "Sending to coq now" in let route_id = 0 in @@ -852,7 +829,7 @@ object(self) let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); - messages#add (Pp.str ("Unsuccessfully tried: "^phrase)); + messages#default_route#add (Pp.str ("Unsuccessfully tried: "^phrase)); more | Good () -> stop Tags.Script.processed in @@ -882,7 +859,7 @@ object(self) buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input"); Sentence.tag_all buffer; (* clear the views *) - messages#clear; + messages#default_route#clear; proof#clear (); clear_info (); processed <- 0; diff --git a/ide/coqOps.mli b/ide/coqOps.mli index ce983c882..3685fea92 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -9,6 +9,7 @@ (************************************************************************) open Coq +open Interface class type ops = object @@ -18,7 +19,8 @@ object method process_next_phrase : unit task method process_until_end_or_error : unit task method handle_reset_initial : unit task - method raw_coq_query : string -> unit task + method raw_coq_query : + route_id:int -> next:(query_rty value -> unit task) -> string -> unit task method show_goals : unit task method backtrack_last_phrase : unit task method initialize : unit task @@ -30,7 +32,7 @@ object method get_slaves_status : int * int * string CString.Map.t - method handle_failure : Interface.handle_exn_rty -> unit task + method handle_failure : handle_exn_rty -> unit task method destroy : unit -> unit end @@ -38,7 +40,7 @@ end class coqops : Wg_ScriptView.script_view -> Wg_ProofView.proof_view -> - Wg_MessageView.message_view -> + Wg_RoutedMessageViews.message_views_router -> Wg_Segment.segment -> coqtop -> (unit -> string option) -> diff --git a/ide/coqide.ml b/ide/coqide.ml index 82b7ba32c..aa816f2b8 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -332,10 +332,10 @@ let export kind sn = local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1" in - sn.messages#set (Pp.str ("Running: "^cmd)); + sn.messages#default_route#set (Pp.str ("Running: "^cmd)); let finally st = flash_info (cmd ^ pr_exit_status st) in - run_command (fun msg -> sn.messages#add_string msg) finally cmd + run_command (fun msg -> sn.messages#default_route#add_string msg) finally cmd let export kind = cb_on_current_term (export kind) @@ -447,9 +447,9 @@ let compile sn = ^ " " ^ (Filename.quote f) ^ " 2>&1" in let buf = Buffer.create 1024 in - sn.messages#set (Pp.str ("Running: "^cmd)); + sn.messages#default_route#set (Pp.str ("Running: "^cmd)); let display s = - sn.messages#add_string s; + sn.messages#default_route#add_string s; Buffer.add_string buf s in let finally st = @@ -457,8 +457,8 @@ let compile sn = flash_info (f ^ " successfully compiled") else begin flash_info (f ^ " failed to compile"); - sn.messages#set (Pp.str "Compilation output:\n"); - sn.messages#add (Pp.str (Buffer.contents buf)); + sn.messages#default_route#set (Pp.str "Compilation output:\n"); + sn.messages#default_route#add (Pp.str (Buffer.contents buf)); end in run_command display finally cmd @@ -480,13 +480,13 @@ let make sn = |Some f -> File.saveall (); let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in - sn.messages#set (Pp.str "Compilation output:\n"); + sn.messages#default_route#set (Pp.str "Compilation output:\n"); Buffer.reset last_make_buf; last_make := ""; last_make_index := 0; last_make_dir := Filename.dirname f; let display s = - sn.messages#add_string s; + sn.messages#default_route#add_string s; Buffer.add_string last_make_buf s in let finally st = flash_info (cmd_make#get ^ pr_exit_status st) @@ -524,11 +524,11 @@ let next_error sn = let stopi = b#get_iter_at_byte ~line:(line-1) stop in b#apply_tag Tags.Script.error ~start:starti ~stop:stopi; b#place_cursor ~where:starti; - sn.messages#set (Pp.str error_msg); + sn.messages#default_route#set (Pp.str error_msg); sn.script#misc#grab_focus () with Not_found -> last_make_index := 0; - sn.messages#set (Pp.str "No more errors.\n") + sn.messages#default_route#set (Pp.str "No more errors.\n") let next_error = cb_on_current_term next_error @@ -609,16 +609,14 @@ let get_current_word term = (** Then look at the current selected word *) let buf1 = term.script#buffer in let buf2 = term.proof#buffer in - let buf3 = term.messages#buffer in if buf1#has_selection then let (start, stop) = buf1#selection_bounds in buf1#get_text ~slice:true ~start ~stop () else if buf2#has_selection then let (start, stop) = buf2#selection_bounds in buf2#get_text ~slice:true ~start ~stop () - else if buf3#has_selection then - let (start, stop) = buf3#selection_bounds in - buf3#get_text ~slice:true ~start ~stop () + else if term.messages#has_selection then + term.messages#get_selected_text (** Otherwise try to find the word around the cursor *) else let it = term.script#buffer#get_iter_at_mark `INSERT in @@ -668,36 +666,18 @@ let match_callback = cb_on_current_term match_callback module Query = struct -let searchabout sn = - let word = get_current_word sn in - let buf = sn.messages#buffer in - let insert result = - let qualid = result.Interface.coq_object_qualid in - let name = String.concat "." qualid in - let tpe = result.Interface.coq_object_object in - buf#insert ~tags:[Tags.Message.item] name; - buf#insert "\n"; - buf#insert tpe; - buf#insert "\n"; - in - let display_results r = - sn.messages#clear; - List.iter insert (match r with Interface.Good l -> l | _ -> []); - Coq.return () - in - let launch_query = - let search = Coq.search [Interface.SubType_Pattern word, true] in - Coq.bind search display_results - in - Coq.try_grab sn.coqtop launch_query ignore - -let searchabout () = on_current_term searchabout - let doquery query sn = - sn.messages#clear; - Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore - -let otherquery command sn = + sn.messages#default_route#clear; + Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query ~route_id:0 + ~next:(function + | Interface.Fail (_, _, err) -> + let err = Ideutils.validate err in + sn.messages#default_route#add err; + Coq.return () + | Interface.Good () -> Coq.return ())) + ignore + +let queryif command sn = Option.iter (fun query -> doquery (query ^ ".") sn) begin try let i = CString.string_index_from command 0 "..." in @@ -706,12 +686,7 @@ let otherquery command sn = else Some (CString.sub command 0 i ^ " " ^ word) with Not_found -> Some command end -let otherquery command = cb_on_current_term (otherquery command) - -let query command _ = - if command = "Search" || command = "SearchAbout" - then searchabout () - else otherquery command () +let query command _ = cb_on_current_term (queryif command) () end @@ -740,7 +715,7 @@ let initial_about () = else "" in let msg = initial_string ^ version_info ^ log_file_message () in - on_current_term (fun term -> term.messages#add_string msg) + on_current_term (fun term -> term.messages#default_route#add_string msg) let coq_icon () = (* May raise Nof_found *) @@ -804,8 +779,8 @@ let coqtop_arguments sn = | args -> let args = String.concat " " args in let msg = Printf.sprintf "Invalid arguments: %s" args in - let () = sn.messages#clear in - sn.messages#push Feedback.Error (Pp.str msg) + let () = sn.messages#default_route#clear in + sn.messages#default_route#push Feedback.Error (Pp.str msg) else dialog#destroy () in let _ = entry#connect#activate ~callback:ok_cb in @@ -1177,17 +1152,17 @@ let build_ui () = item "Help" ~label:"_Help"; item "Browse Coq Manual" ~label:"Browse Coq _Manual" ~callback:(fun _ -> - browse notebook#current_term.messages#add_string (doc_url ())); + browse notebook#current_term.messages#default_route#add_string (doc_url ())); item "Browse Coq Library" ~label:"Browse Coq _Library" ~callback:(fun _ -> - browse notebook#current_term.messages#add_string library_url#get); + browse notebook#current_term.messages#default_route#add_string library_url#get); item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP ~callback:(fun _ -> on_current_term (fun sn -> - browse_keyword sn.messages#add_string (get_current_word sn))); + browse_keyword sn.messages#default_route#add_string (get_current_word sn))); item "Help for μPG mode" ~label:"Help for μPG mode" ~callback:(fun _ -> on_current_term (fun sn -> - sn.messages#clear; - sn.messages#add_string (NanoPG.get_documentation ()))); + sn.messages#default_route#clear; + sn.messages#default_route#add_string (NanoPG.get_documentation ()))); item "About Coq" ~label:"_About" ~stock:`ABOUT ~callback:MiscMenu.about ]; diff --git a/ide/ide.mllib b/ide/ide.mllib index 57e9fe5ad..96ea8c410 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -26,15 +26,16 @@ Gtk_parsing Wg_Segment Wg_ProofView Wg_MessageView +Wg_RoutedMessageViews Wg_Detachable Wg_Find Wg_Completion Wg_ScriptView Coq_commands -Wg_Command FileOps Document CoqOps +Wg_Command Session Coqide_ui NanoPG diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 178695759..bdb39e94a 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -473,3 +473,15 @@ let browse_keyword prerr text = let u = Lazy.force url_for_keyword text in browse prerr (doc_url() ^ u) with Not_found -> prerr ("No documentation found for \""^text^"\".\n") + +let rec is_valid (s : Pp.t) = match Pp.repr s with + | Pp.Ppcmd_empty + | Pp.Ppcmd_print_break _ + | Pp.Ppcmd_force_newline -> true + | Pp.Ppcmd_glue l -> List.for_all is_valid l + | Pp.Ppcmd_string s -> Glib.Utf8.validate s + | Pp.Ppcmd_box (_,s) + | Pp.Ppcmd_tag (_,s) -> is_valid s + | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s +let validate s = + if is_valid s then s else Pp.str "This error massage can't be printed." diff --git a/ide/ideutils.mli b/ide/ideutils.mli index babbfe2f2..0031c59c1 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -98,3 +98,7 @@ val io_read_all : Glib.Io.channel -> string val run_command : (string -> unit) -> (Unix.process_status -> unit) -> string -> unit + +(* Checks if an error message is printable, it not replaces it with + * a printable error *) +val validate : Pp.t -> Pp.t diff --git a/ide/session.ml b/ide/session.ml index 210fbdec4..be2bfe060 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -33,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; @@ -366,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 @@ -390,7 +390,7 @@ let create file coqtop_args = 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 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 @@ -511,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 ) diff --git a/ide/session.mli b/ide/session.mli index e99f08024..bb3816900 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -31,7 +31,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; diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 3ce2c484f..8eddfb314 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -10,7 +10,7 @@ open Preferences -class command_window name coqtop coqops = +class command_window name coqtop coqops router = let frame = Wg_Detachable.detachable ~title:(Printf.sprintf "Query pane (%s)" name) () in let _ = frame#hide in @@ -23,6 +23,10 @@ class command_window name coqtop coqops = notebook#misc#set_size_request ~width:600 ~height:500 (); notebook#misc#grab_focus ()) in + let route_id = + let r = ref 0 in + fun () -> incr r; !r in + object(self) val frame = frame @@ -54,11 +58,13 @@ object(self) method private new_query_aux ?command ?term ?(grab_now=true) () = let frame = GBin.frame ~shadow_type:`NONE () in ignore(notebook#insert_page ~pos:(notebook#page_num new_page) frame#coerce); + let route_id = route_id () in let new_tab_lbl text = let hbox = GPack.hbox ~homogeneous:false () in ignore(GMisc.label ~width:100 ~ellipsize:`END ~text ~packing:hbox#pack()); let b = GButton.button ~packing:hbox#pack () in ignore(b#connect#clicked ~callback:(fun () -> + router#delete_route route_id; views <- List.filter (fun (f,_,_) -> f#get_oid <> frame#coerce#get_oid) views; notebook#remove_page (notebook#page_num frame#coerce))); @@ -90,7 +96,9 @@ object(self) ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(vbox#pack ~fill:true ~expand:true) () in - let result = GText.view ~packing:r_bin#add () in + let result = Wg_MessageView.message_view () in + router#register_route route_id result; + r_bin#add (result :> GObj.widget); views <- (frame#coerce, result, combo#entry) :: views; let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in let _ = background_color#connect#changed ~callback:cb in @@ -98,7 +106,6 @@ object(self) let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in stick text_font result cb; result#misc#set_can_focus true; (* false causes problems for selection *) - result#set_editable false; let callback () = let com = combo#entry#text in let arg = entry#text in @@ -108,22 +115,19 @@ object(self) else com ^ " " ^ arg ^" . " in let process = - (* We need to adapt this to route_id and redirect to the result buffer below *) - coqops#raw_coq_query phrase - (* - Coq.bind (Coq.query (phrase,sid)) (function - | Interface.Fail (_,l,str) -> - let width = Ideutils.textview_width result in - Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str); + let next = function + | Interface.Fail (_, _, err) -> + let err = Ideutils.validate err in + result#set err; notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; - Coq.return () - | Interface.Good res -> - result#buffer#insert res; + Coq.return () + | Interface.Good () -> notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce; - Coq.return ()) - *) + Coq.return () + in + coqops#raw_coq_query ~route_id ~next phrase in - result#buffer#set_text ("Result for command " ^ phrase ^ ":\n"); + result#set (Pp.str ("Result for command " ^ phrase ^ ":\n")); Coq.try_grab coqtop process ignore in ignore (combo#entry#connect#activate ~callback); diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli index c70a95761..1e0eb675c 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -class command_window : string -> Coq.coqtop -> CoqOps.coqops -> +class command_window : string -> Coq.coqtop -> CoqOps.coqops -> Wg_RoutedMessageViews.message_views_router -> object method new_query : ?command:string -> ?term:string -> unit -> unit method pack_in : (GObj.widget -> unit) -> unit diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 74f687ef7..a79a093e3 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -36,8 +36,8 @@ class type message_view = method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) - method buffer : GText.buffer - (** for more advanced text edition *) + method has_selection : bool + method get_selected_text : string end let message_view () : message_view = @@ -45,7 +45,6 @@ let message_view () : message_view = ~highlight_matching_brackets:true ~tag_table:Tags.Message.table () in - let text_buffer = new GText.buffer buffer#as_buffer in let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in let box = GPack.vbox () in let scroll = GBin.scrolled_window @@ -120,7 +119,12 @@ let message_view () : message_view = method set msg = self#clear; self#add msg - method buffer = text_buffer + method has_selection = buffer#has_selection + method get_selected_text = + if buffer#has_selection then + let start, stop = buffer#selection_bounds in + buffer#get_text ~slice:true ~start ~stop () + else "" end in diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index e7ec3c578..472aaf5ed 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -26,8 +26,8 @@ class type message_view = method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) - method buffer : GText.buffer - (** for more advanced text edition *) + method has_selection : bool + method get_selected_text : string end val message_view : unit -> message_view diff --git a/ide/wg_RoutedMessageViews.ml b/ide/wg_RoutedMessageViews.ml new file mode 100644 index 000000000..4bd303524 --- /dev/null +++ b/ide/wg_RoutedMessageViews.ml @@ -0,0 +1,47 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Wg_MessageView.message_view + method default_route : Wg_MessageView.message_view + + method has_selection : bool + method get_selected_text : string + + method register_route : int -> Wg_MessageView.message_view -> unit + method delete_route : int -> unit +end + +let message_views ~route_0 : message_views_router = + let route_table = Hashtbl.create 17 in + let () = Hashtbl.add route_table 0 route_0 in +object + method route i = + try Hashtbl.find route_table i + with Not_found -> + (* at least the message will be printed somewhere*) + Hashtbl.find route_table 0 + + method default_route = route_0 + + method register_route i mv = Hashtbl.add route_table i mv + + method delete_route i = Hashtbl.remove route_table i + + method has_selection = + Hashtbl.fold (fun _ v -> (||) v#has_selection) route_table false + + method get_selected_text = + Option.default "" + (Hashtbl.fold (fun _ v acc -> + if v#has_selection then Some v#get_selected_text else acc) + route_table None) + +end diff --git a/ide/wg_RoutedMessageViews.mli b/ide/wg_RoutedMessageViews.mli new file mode 100644 index 000000000..cca43d55b --- /dev/null +++ b/ide/wg_RoutedMessageViews.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Wg_MessageView.message_view + method default_route : Wg_MessageView.message_view + + method has_selection : bool + method get_selected_text : string + + method register_route : int -> Wg_MessageView.message_view -> unit + method delete_route : int -> unit +end + +val message_views : + route_0:Wg_MessageView.message_view -> message_views_router -- cgit v1.2.3