From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- ide/coqOps.ml | 272 ++++++++++++++++++++++++++-------------------------------- 1 file changed, 123 insertions(+), 149 deletions(-) (limited to 'ide/coqOps.ml') diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 1563c7ff..6c3438a4 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* mem_flag = function | `ERROR _ -> `ERROR @@ -58,7 +60,7 @@ module SentenceId : sig val connect : sentence -> signals val dbg_to_string : - GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.std_ppcmds + GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.t end = struct @@ -117,7 +119,7 @@ end = struct (b#get_iter_at_mark s.start)#offset (b#get_iter_at_mark s.stop)#offset (ellipsize - ((b#get_iter_at_mark s.start)#get_slice (b#get_iter_at_mark s.stop))) + ((b#get_iter_at_mark s.start)#get_slice ~stop:(b#get_iter_at_mark s.stop))) (String.concat "," (List.map str_of_flag s.flags)) (ellipsize (String.concat "," @@ -139,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 @@ -162,14 +165,6 @@ let flags_to_color f = else if List.mem `INCOMPLETE f then `NAME "gray" else `NAME Preferences.processed_color#get -let validate s = - let open Xml_datatype in - let rec validate = function - | PCData s -> Glib.Utf8.validate s - | Element (_, _, children) -> List.for_all validate children - in - validate (Richpp.repr s) - module Doc = Document let segment_model (doc : sentence Doc.document) : Wg_Segment.model = @@ -201,7 +196,7 @@ object (self) in List.iter (fun s -> set_index s (s.index + 1)) after; set_index s (document_length - List.length after); - ignore ((SentenceId.connect s)#changed self#on_changed); + ignore ((SentenceId.connect s)#changed ~callback:self#on_changed); document_length <- document_length + 1; List.iter (fun f -> f `INSERT) cbs @@ -215,8 +210,8 @@ object (self) List.iter (fun f -> f `REMOVE) cbs initializer - let _ = (Doc.connect doc)#pushed self#on_push in - let _ = (Doc.connect doc)#popped self#on_pop in + let _ = (Doc.connect doc)#pushed ~callback:self#on_push in + let _ = (Doc.connect doc)#popped ~callback:self#on_pop in () end @@ -224,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 = @@ -267,15 +262,15 @@ object(self) else iter in let iter = sentence_start iter in - script#buffer#place_cursor iter; + script#buffer#place_cursor ~where:iter; ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter) in - let _ = segment#connect#clicked on_click in + let _ = segment#connect#clicked ~callback:on_click in () method private tooltip_callback ~x ~y ~kbd tooltip = - let x, y = script#window_to_buffer_coords `WIDGET x y in - let iter = script#get_iter_at_location x y in + let x, y = script#window_to_buffer_coords ~tag:`WIDGET ~x ~y in + let iter = script#get_iter_at_location ~x ~y in if iter#has_tag Tags.Script.tooltip then begin let s = let rec aux iter = @@ -305,7 +300,7 @@ object(self) method private print_stack = Minilib.log "document:"; - Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer))) + Minilib.log_pp (Doc.print document (dbg_to_string buffer)) method private enter_focus start stop = let at id id' _ = Stateid.equal id' id in @@ -337,7 +332,6 @@ object(self) buffer#get_iter_at_mark `INSERT method private show_goals_aux ?(move_insert=false) () = - Coq.PrintOpt.set_printing_width proof#width; if move_insert then begin let dest = self#get_start_of_input in if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin @@ -345,7 +339,7 @@ object(self) script#recenter_insert end end; - Coq.bind (Coq.goals ~logger:messages#push ()) (function + Coq.bind (Coq.goals ()) (function | Fail x -> self#handle_failure_aux ~move_insert x | Good goals -> Coq.bind (Coq.evars ()) (function @@ -353,32 +347,28 @@ object(self) | Good evs -> proof#set_goals goals; proof#set_evars evs; - proof#refresh (); + proof#refresh ~force:true; Coq.return () ) ) method show_goals = self#show_goals_aux () (* This method is intended to perform stateless commands *) - method raw_coq_query phrase = - 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 = - Coq.query ~logger:messages#push (phrase,Stateid.dummy) in - let next = function - | Fail (_, _, err) -> display_error err; Coq.return () - | Good msg -> - messages#add_string msg; Coq.return () + 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 query = Coq.query (route_id,(phrase,sid)) in Coq.bind (Coq.seq action query) next + method private still_valid { edit_id = id } = + try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true + with Not_found -> false + method private mark_as_needed sentence = - Minilib.log("Marking " ^ - Pp.string_of_ppcmds (dbg_to_string buffer false None sentence)); + if self#still_valid sentence then begin + Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence); let start = buffer#get_iter_at_mark sentence.start in let stop = buffer#get_iter_at_mark sentence.stop in let to_process = Tags.Script.to_process in @@ -398,11 +388,11 @@ object(self) in List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags; List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags + end - method private attach_tooltip sentence loc text = + method private attach_tooltip ?loc sentence text = let start_sentence, stop_sentence, phrase = self#get_sentence sentence in - let pre_chars, post_chars = - if Loc.is_ghost loc then 0, String.length phrase else Loc.unloc loc in + let pre_chars, post_chars = Option.cata Loc.unloc (0, String.length phrase) loc in let pre = b2c phrase pre_chars in let post = b2c phrase post_chars in let start = start_sentence#forward_chars pre in @@ -411,95 +401,93 @@ object(self) buffer#apply_tag Tags.Script.tooltip ~start ~stop; add_tooltip sentence pre post markup - method private is_dummy_id id = - match id with - | Edit 0 -> true - | State id when Stateid.equal id Stateid.dummy -> true - | _ -> false - method private enqueue_feedback msg = - let id = msg.id in - if self#is_dummy_id id then () else Queue.add msg feedbacks - + (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt Xmlprotocol.(of_feedback Ppcmds msg)); *) + Queue.add msg feedbacks + method private process_feedback () = let rec eat_feedback n = if n = 0 then true else let msg = Queue.pop feedbacks in - let id = msg.id in + let id = msg.span_id in let sentence = let finder _ state_id s = match state_id, id with - | Some id', State id when Stateid.equal id id' -> Some (state_id, s) - | _, Edit id when id = s.edit_id -> Some (state_id, s) + | Some id', id when Stateid.equal id id' -> Some (state_id, s) | _ -> None in try Some (Doc.find_map document finder) with Not_found -> None in - let log s state_id = - Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string - (Option.default Stateid.dummy state_id)) in + let log_pp ?id s= + Minilib.log_pp Pp.(seq + [str "Feedback "; s; pr_opt (fun id -> str " on " ++ str (Stateid.to_string id)) id]) + in + let log ?id s = log_pp ?id (Pp.str s) in begin match msg.contents, sentence with | AddedAxiom, Some (id,sentence) -> - log "AddedAxiom" id; + log ?id "AddedAxiom"; remove_flag sentence `PROCESSING; remove_flag sentence `ERROR; add_flag sentence `UNSAFE; self#mark_as_needed sentence | Processed, Some (id,sentence) -> - log "Processed" id; + log ?id "Processed" ; remove_flag sentence `PROCESSING; self#mark_as_needed sentence | ProcessingIn _, Some (id,sentence) -> - log "ProcessingIn" id; + log ?id "ProcessingIn"; add_flag sentence `PROCESSING; self#mark_as_needed sentence | Incomplete, Some (id, sentence) -> - log "Incomplete" id; + log ?id "Incomplete"; add_flag sentence `INCOMPLETE; self#mark_as_needed sentence | Complete, Some (id, sentence) -> - log "Complete" id; + log ?id "Complete"; remove_flag sentence `INCOMPLETE; self#mark_as_needed sentence | GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) -> - log "GlobRef" id; - self#attach_tooltip sentence loc + log ?id "GlobRef"; + self#attach_tooltip ~loc sentence (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> - let loc = Option.default Loc.ghost loc in - let msg = Richpp.raw_print msg in - log "ErrorMsg" id; + log_pp ?id Pp.(str "ErrorMsg " ++ msg); remove_flag sentence `PROCESSING; - add_flag sentence (`ERROR (loc, msg)); + let rmsg = Pp.string_of_ppcmds msg in + add_flag sentence (`ERROR (loc, rmsg)); self#mark_as_needed sentence; - self#attach_tooltip sentence loc msg; - if not (Loc.is_ghost loc) then - self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) - | Message(Warning, loc, msg), Some (id,sentence) -> - let loc = Option.default Loc.ghost loc in - let msg = Richpp.raw_print msg in - log "WarningMsg" id; - add_flag sentence (`WARNING (loc, msg)); - self#attach_tooltip sentence loc msg; - self#position_warning_tag_at_sentence sentence loc - | Message((Info|Notice|Debug as lvl), _, msg), _ -> - messages#push lvl msg + self#attach_tooltip ?loc sentence rmsg; + self#position_tag_at_sentence ?loc Tags.Script.error sentence + | 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#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, 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 | WorkerStatus(id,status), _ -> - log "WorkerStatus" None; + log "WorkerStatus"; slaves_status <- CString.Map.add id status slaves_status - | _ -> if sentence <> None then Minilib.log "Unsupported feedback message" else if Doc.is_empty document then () else try match id, Doc.tip document with - | Edit _, _ -> () - | State id1, id2 when Stateid.newer_than id2 id1 -> () + | id1, id2 when Stateid.newer_than id2 id1 -> () | _ -> Queue.add msg feedbacks - with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks + with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks end; eat_feedback (n-1) in @@ -513,40 +501,30 @@ object(self) let stop = buffer#get_iter_at_mark sentence.stop in buffer#move_mark ~where:stop (`NAME "start_of_input"); - method private position_error_tag_at_iter iter phrase = function - | None -> () - | Some (start, stop) -> - buffer#apply_tag Tags.Script.error - ~start:(iter#forward_chars (b2c phrase start)) - ~stop:(iter#forward_chars (b2c phrase stop)) - - method private position_error_tag_at_sentence sentence loc = - let start, _, phrase = self#get_sentence sentence in - self#position_error_tag_at_iter start phrase loc - - method private position_warning_tag_at_iter iter_start iter_stop phrase loc = - if Loc.is_ghost loc then - buffer#apply_tag Tags.Script.warning ~start:iter_start ~stop:iter_stop - else - buffer#apply_tag Tags.Script.warning - ~start:(iter_start#forward_chars (b2c phrase loc.Loc.bp)) - ~stop:(iter_stop#forward_chars (b2c phrase loc.Loc.ep)) + method private position_tag_at_iter ?loc iter_start iter_stop tag phrase = match loc with + | None -> + buffer#apply_tag tag ~start:iter_start ~stop:iter_stop + | Some loc -> + let start, stop = Loc.unloc loc in + buffer#apply_tag tag + ~start:(iter_start#forward_chars (b2c phrase start)) + ~stop:(iter_start#forward_chars (b2c phrase stop)) - method private position_warning_tag_at_sentence sentence loc = + method private position_tag_at_sentence ?loc tag sentence = let start, stop, phrase = self#get_sentence sentence in - self#position_warning_tag_at_iter start stop phrase loc + self#position_tag_at_iter ?loc start stop tag phrase - method private process_interp_error queue sentence loc msg tip id = + method private process_interp_error ?loc queue sentence msg tip id = Coq.bind (Coq.return ()) (function () -> let start, stop, phrase = self#get_sentence sentence in buffer#remove_tag Tags.Script.to_process ~start ~stop; self#discard_command_queue queue; pop_info (); if Stateid.equal id tip || Stateid.equal id Stateid.dummy then begin - self#position_error_tag_at_iter start phrase loc; + 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 () @@ -604,12 +582,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] @@ -628,10 +606,9 @@ object(self) if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> - - logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted"); + logger Feedback.Error (Pp.str "You must close the proof with Qed or Admitted"); self#discard_command_queue queue; - conclude [] + conclude [] | `Skip(start,stop), (_,s) :: topstack -> assert(start#equal (buffer#get_iter_at_mark s.start)); assert(stop#equal (buffer#get_iter_at_mark s.stop)); @@ -641,11 +618,11 @@ object(self) add_flag sentence `PROCESSING; Doc.push document sentence; let _, _, phrase = self#get_sentence sentence in - let coq_query = Coq.add ~logger ((phrase,edit_id),(tip,verbose)) in + let coq_query = Coq.add ((phrase,edit_id),(tip,verbose)) in let handle_answer = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> Doc.assign_tip_id document id; - logger Feedback.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Pp.str msg); self#commit_queue_transaction sentence; loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> @@ -653,13 +630,14 @@ object(self) let topstack, _ = Doc.context document in self#exit_focus; self#cleanup (Doc.cut_at document tip); - logger Feedback.Notice (Richpp.richpp_of_string msg); + logger Feedback.Notice (Pp.str msg); self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) | Fail (id, loc, msg) -> + let loc = Option.map Loc.make_loc loc in let sentence = Doc.pop document in - self#process_interp_error queue sentence loc msg tip id in + self#process_interp_error ?loc queue sentence msg tip id in Coq.bind coq_query handle_answer in let tip = @@ -667,15 +645,16 @@ object(self) with Doc.Empty -> initial_state | Invalid_argument _ -> assert false in loop tip [] in Coq.bind fill_queue process_queue - + method join_document = let next = function | Good _ -> - messages#clear; - messages#push Feedback.Info (Richpp.richpp_of_string "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 ~logger:messages#push true) next + Coq.bind (Coq.status true) next method stop_worker n = Coq.bind (Coq.stop_worker n) (fun _ -> Coq.return ()) @@ -689,14 +668,13 @@ object(self) let extract_error s = match List.find (function `ERROR _ -> true | _ -> false) s.flags with | `ERROR (loc, msg) -> - let iter = - if Loc.is_ghost loc then - buffer#get_iter_at_mark s.start - else + let iter = begin match loc with + | None -> buffer#get_iter_at_mark s.start + | Some loc -> let (iter, _, phrase) = self#get_sentence s in let (start, _) = Loc.unloc loc in - iter#forward_chars (b2c phrase start) in - iter#line + 1, msg + iter#forward_chars (b2c phrase start) + end in iter#line + 1, msg | _ -> assert false in List.rev (Doc.fold_all document [] (fun acc _ _ s -> @@ -775,7 +753,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)) @@ -792,7 +770,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 @@ -804,7 +782,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 @@ -812,7 +790,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 @@ -820,7 +798,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) @@ -845,25 +823,21 @@ 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 query = Coq.query (phrase,Stateid.dummy) in + let route_id = 0 in + let query = Coq.query (route_id,(phrase,Stateid.dummy)) in let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); - messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase)); + messages#default_route#add (Pp.str ("Unsuccessfully tried: "^phrase)); more - | Good msg -> - messages#add_string msg; - stop Tags.Script.processed + | Good () -> stop Tags.Script.processed in Coq.bind (Coq.seq action query) next in @@ -891,7 +865,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; @@ -905,7 +879,7 @@ object(self) let get_initial_state = let next = function | Fail (_, _, message) -> - let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in + let message = "Couldn't initialize coqtop\n\n" ^ (Pp.string_of_ppcmds message) in let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in ignore (popup#run ()); exit 1 | Good id -> initial_state <- id; Coq.return () in -- cgit v1.2.3