aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coqOps.ml85
-rw-r--r--ide/coqOps.mli8
-rw-r--r--ide/coqide.ml89
-rw-r--r--ide/ide.mllib3
-rw-r--r--ide/ideutils.ml12
-rw-r--r--ide/ideutils.mli4
-rw-r--r--ide/session.ml10
-rw-r--r--ide/session.mli2
-rw-r--r--ide/wg_Command.ml36
-rw-r--r--ide/wg_Command.mli2
-rw-r--r--ide/wg_MessageView.ml12
-rw-r--r--ide/wg_MessageView.mli4
-rw-r--r--ide/wg_RoutedMessageViews.ml47
-rw-r--r--ide/wg_RoutedMessageViews.mli23
14 files changed, 193 insertions, 144 deletions
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 *)
+(* <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 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+class type message_views_router = object
+ method route : int -> 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 *)
+(* <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 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+class type message_views_router = object
+ method route : int -> 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 07:42:08 +0000