1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \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) *)
(************************************************************************)
open Util
open Coq
open Ideutils
open Interface
open Feedback
let b2c = byte_offset_to_char_offset
(** variant of buffer_off_to_byte_off: convert unicode offset (used by GTK buffer)
to UTF-8 byte offset (used by Coq) with size caching for performance *)
let c2b (buffer : GText.buffer) (s_byte, s_uni) uni_off =
if s_uni < 0 then
raise (invalid_arg "c2b: s_uni must be >= 0");
let rec cvt iter rv =
if iter#offset <= s_uni then
rv
else
cvt iter#backward_char (rv + (ulen iter#char))
in
cvt (buffer#get_iter (`OFFSET uni_off)) s_byte
type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string Loc.located | `WARNING of string Loc.located ]
type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ]
let mem_flag_of_flag : flag -> mem_flag = function
| `ERROR _ -> `ERROR
| `WARNING _ -> `WARNING
| (`INCOMPLETE | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag
let str_of_flag = function
| `UNSAFE -> "U"
| `PROCESSING -> "P"
| `ERROR _ -> "E"
| `WARNING _ -> "W"
| `INCOMPLETE -> "I"
class type signals =
object
inherit GUtil.ml_signals
method changed : callback:(int * mem_flag list -> unit) -> GtkSignal.id
end
module SentenceId : sig
type sentence = {
start : GText.mark;
stop : GText.mark;
mutable byte_start : int;
mutable flags : flag list;
mutable tooltips : (int * int * string) list;
edit_id : int;
mutable index : int;
changed_sig : (int * mem_flag list) GUtil.signal;
}
val mk_sentence :
start:GText.mark -> stop:GText.mark -> flag list -> sentence
val add_flag : sentence -> flag -> unit
val has_flag : sentence -> mem_flag -> bool
val remove_flag : sentence -> mem_flag -> unit
val find_all_tooltips : sentence -> int -> string list
val add_tooltip : sentence -> int -> int -> string -> unit
val set_index : sentence -> int -> unit
val connect : sentence -> signals
val dbg_to_string :
GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.t
end = struct
type sentence = {
start : GText.mark;
stop : GText.mark;
mutable byte_start : int;
mutable flags : flag list;
mutable tooltips : (int * int * string) list;
edit_id : int;
mutable index : int;
changed_sig : (int * mem_flag list) GUtil.signal;
}
let connect s : signals =
object
inherit GUtil.ml_signals [s.changed_sig#disconnect]
method changed = s.changed_sig#connect ~after
end
let id = ref 0
let mk_sentence ~start ~stop flags = decr id; {
start = start;
stop = stop;
byte_start = 0;
flags = flags;
edit_id = !id;
tooltips = [];
index = -1;
changed_sig = new GUtil.signal ();
}
let changed s =
s.changed_sig#call (s.index, List.map mem_flag_of_flag s.flags)
let add_flag s f = s.flags <- CList.add_set (=) f s.flags; changed s
let has_flag s mf =
List.exists (fun f -> mem_flag_of_flag f = mf) s.flags
let remove_flag s mf =
s.flags <- List.filter (fun f -> mem_flag_of_flag f <> mf) s.flags; changed s
let find_all_tooltips s off =
CList.map_filter (fun (start,stop,t) ->
if start <= off && off <= stop then Some t else None)
s.tooltips
let add_tooltip s a b t = s.tooltips <- (a,b,t) :: s.tooltips
let set_index s i = s.index <- i
let dbg_to_string (b : GText.buffer) focused id s =
let ellipsize s =
Str.global_replace (Str.regexp "^[\n ]*") ""
(if String.length s > 20 then String.sub s 0 17 ^ "..."
else s) in
Pp.str (Printf.sprintf "%s[%3d,%3s](%5d,%5d) %s [%s] %s"
(if focused then "*" else " ")
s.edit_id
(Stateid.to_string (Option.default Stateid.dummy id))
(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 ~stop:(b#get_iter_at_mark s.stop)))
(String.concat "," (List.map str_of_flag s.flags))
(ellipsize
(String.concat ","
(List.map (fun (a,b,t) ->
Printf.sprintf "<%d,%d> %s" a b t) s.tooltips))))
end
open SentenceId
let log msg : unit task =
Coq.lift (fun () -> Minilib.log msg)
class type ops =
object
method go_to_insert : unit task
method go_to_mark : GText.mark -> unit task
method process_next_phrase : unit task
method process_db_cmd : string ->
next:(Interface.db_cmd_rty Interface.value -> unit task) -> unit task
method process_db_configd : unit ->
next:(Interface.db_configd_rty Interface.value -> unit task) -> unit task
method process_db_upd_bpts : ((string * int) * bool) list ->
next:(Interface.db_upd_bpts_rty Interface.value -> unit task) -> unit task
method process_db_continue : db_continue_opt ->
next:(Interface.db_continue_rty Interface.value -> unit task) -> unit task
method process_db_stack :
next:(Interface.db_stack_rty Interface.value -> unit task) -> unit task
method process_db_vars : int ->
next:(Interface.db_vars_rty Interface.value -> unit task) -> unit task
method process_until_end_or_error : unit task
method handle_reset_initial : unit task
method raw_coq_query :
route_id:int -> next:(query_rty value -> unit task) -> string -> unit task
method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task
method show_goals : unit task
method backtrack_last_phrase : unit task
method initialize : unit task
method join_document : unit task
method stop_worker : string -> unit task
method get_n_errors : int
method get_errors : (int * string) list
method get_slaves_status : int * int * string CString.Map.t
method backtrack_to_begin : unit -> unit task
method handle_failure : handle_exn_rty -> unit task
method destroy : unit -> unit
method scroll_to_start_of_input : unit -> unit
method set_forward_clear_db_highlight : (unit -> unit) -> unit
method set_forward_set_goals_of_dbg_session : (Pp.t -> unit) -> unit
method set_forward_init_db : (unit -> unit) -> unit
method set_debug_goal : Pp.t -> unit
end
let flags_to_color f =
if List.mem `PROCESSING f then `NAME "blue"
else if List.mem `ERROR f then `NAME "red"
else if List.mem `UNSAFE f then `NAME "orange"
else if List.mem `INCOMPLETE f then `NAME "gray"
else `NAME Preferences.processed_color#get
module Doc = Document
let segment_model (doc : sentence Doc.document) : Wg_Segment.model =
object (self)
val mutable cbs = []
val mutable document_length = 0
method length = document_length
method changed ~callback = cbs <- callback :: cbs
method fold : 'a. ('a -> Wg_Segment.color -> 'a) -> 'a -> 'a = fun f accu ->
let fold accu _ _ s =
let flags = List.map mem_flag_of_flag s.flags in
f accu (flags_to_color flags)
in
Doc.fold_all doc accu fold
method private on_changed (i, f) =
let data = (i, flags_to_color f) in
List.iter (fun f -> f (`SET data)) cbs
method private on_push s ctx =
let after = match ctx with
| None -> []
| Some (l, _) -> l
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 ~callback:self#on_changed);
document_length <- document_length + 1;
List.iter (fun f -> f `INSERT) cbs
method private on_pop s ctx =
let () = match ctx with
| None -> ()
| Some (l, _) -> List.iter (fun s -> set_index s (s.index - 1)) l
in
set_index s (-1);
document_length <- document_length - 1;
List.iter (fun f -> f `REMOVE) cbs
initializer
let _ = (Doc.connect doc)#pushed ~callback:self#on_push in
let _ = (Doc.connect doc)#popped ~callback:self#on_pop in
()
end
type queue_msg =
| MsgFeedback of Feedback.feedback
| MsgDebug of string * Pp.t
let rec flatten = function
| [] -> []
| (lg, rg) :: l ->
let inner = flatten l in
List.rev_append lg inner @ rg
class coqops
(_script:Wg_ScriptView.script_view)
(_pv:Wg_ProofView.proof_view)
(_mv:Wg_RoutedMessageViews.message_views_router)
(_sg:Wg_Segment.segment)
(_ct:Coq.coqtop)
get_filename =
object(self)
val script = _script
val buffer = (_script#source_buffer :> GText.buffer)
val proof = _pv
val messages = _mv
val segment = _sg
val document : sentence Doc.document = Doc.create ()
val mutable document_length = 0
val mutable initial_state = Stateid.initial
(* proofs being processed by the slaves *)
val mutable to_process = 0
val mutable processed = 0
val mutable slaves_status = CString.Map.empty
val mutable last_offsets = (0,0)
val mutable forward_clear_db_highlight = ((fun x -> failwith "forward_clear_db_highlight")
: unit -> unit)
val mutable forward_set_goals_of_dbg_session = ((fun x -> failwith "forward_set_goals_of_dbg_session")
: Pp.t -> unit)
val mutable forward_init_db = ((fun x -> failwith "forward_init_db")
: unit -> unit)
initializer
Coq.set_feedback_handler _ct
(fun msg -> self#process_feedback (MsgFeedback msg));
Coq.set_debug_prompt_handler _ct
(fun ~tag msg -> self#process_feedback (MsgDebug (tag, msg)));
script#misc#set_has_tooltip true;
ignore(script#misc#connect#query_tooltip ~callback:self#tooltip_callback);
let md = segment_model document in
segment#set_model md;
let on_click id =
let find _ _ s = Int.equal s.index id in
let sentence = Doc.find document find in
let mark = sentence.start in
let iter = script#buffer#get_iter_at_mark mark in
(* Sentence starts tend to be at the end of a line, so we rather choose
the first non-line-ending position. *)
let rec sentence_start iter =
if iter#ends_line then sentence_start iter#forward_line
else iter
in
let iter = sentence_start iter in
script#buffer#place_cursor ~where:iter;
ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
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 ~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 =
let marks = iter#marks in
if marks = [] then aux iter#backward_char
else
let mem_marks _ _ s =
List.exists (fun m ->
Gobject.get_oid m =
Gobject.get_oid (buffer#get_mark s.start)) marks in
try Doc.find document mem_marks
with Not_found -> aux iter#backward_char in
aux iter in
let ss = find_all_tooltips s iter#offset in
let msg = String.concat "\n" (CList.uniquize ss) in
GtkBase.Tooltip.set_icon_from_stock tooltip `INFO `BUTTON;
script#misc#set_tooltip_markup ("<tt>" ^ msg ^ "</tt>")
end else begin
script#misc#set_tooltip_text ""; script#misc#set_has_tooltip true
end;
false
method destroy () = ()
method scroll_to_start_of_input () =
let start = buffer#get_iter_at_mark (`NAME "start_of_input") in
ignore (script#scroll_to_iter ~use_align:true ~yalign:0. start)
method set_forward_clear_db_highlight f =
forward_clear_db_highlight <- f
method set_forward_set_goals_of_dbg_session f =
forward_set_goals_of_dbg_session <- f
method set_forward_init_db f =
forward_init_db <- f
method private print_stack =
Minilib.log "document:";
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
self#print_stack;
Minilib.log("Focusing "^Stateid.to_string start^" "^Stateid.to_string stop);
Doc.focus document ~cond_top:(at start) ~cond_bot:(at stop);
self#print_stack;
let qed_s = Doc.tip_data document in
buffer#move_mark ~where:(buffer#get_iter_at_mark qed_s.stop)
(`NAME "stop_of_input")
method private exit_focus =
Minilib.log "Unfocusing";
Doc.unfocus document;
self#print_stack;
begin try
let where = buffer#get_iter_at_mark (Doc.tip_data document).stop in
buffer#move_mark ~where (`NAME "start_of_input");
with Doc.Empty -> () end;
buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input")
method private get_start_of_input =
buffer#get_iter_at_mark (`NAME "start_of_input")
method private get_end_of_input =
buffer#get_iter_at_mark (`NAME "stop_of_input")
method private get_insert =
buffer#get_iter_at_mark `INSERT
method private show_goals_aux ?(move_insert=false) () =
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
buffer#place_cursor ~where:dest;
script#recenter_insert
end
end;
let flags = { gf_mode = "full"; gf_fg = true; gf_bg = true; gf_shelved = false; gf_given_up = false } in
let return x = Coq.return (Good x) in
let (>>=) m f = Coq.bind m (function
| Fail x -> Coq.return (Fail x)
| Good v -> f v)
in
let call =
Coq.subgoals flags >>= begin function
| None -> return Wg_ProofView.NoGoals
| Some { fg_goals = ((_ :: _) as fg); bg_goals = bg } ->
let bg = flatten (List.rev bg) in
return (Wg_ProofView.FocusGoals { fg; bg; })
| Some { fg_goals = []; bg_goals = bg } ->
let flags = { gf_mode = "short"; gf_fg = false; gf_bg = false; gf_shelved = true; gf_given_up = true } in
Coq.subgoals flags >>= fun rem ->
let bg = flatten (List.rev bg) in
let shelved, given_up = match rem with
| None -> [], []
| Some goals -> goals.shelved_goals, goals.given_up_goals
in
return (Wg_ProofView.NoFocusGoals { bg; shelved; given_up })
end
in
Coq.bind call begin function
| Fail x -> self#handle_failure_aux ~move_insert x
| Good goals ->
proof#set_goals goals;
proof#refresh ~force:true;
Coq.return ()
end
method show_goals = self#show_goals_aux ()
(* This method is intended to perform stateless commands *)
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 proof_diff where ~next : unit Coq.task =
(* todo: would be nice to ignore comments, too *)
let rec back iter =
if iter#is_start then iter
else
let c = iter#char in
if Glib.Unichar.isspace c || c = 0 then back (iter#backward_char)
else if c = int_of_char '.' then iter#backward_char
else iter in
let where = back (buffer#get_iter_at_mark where) in
let until _ start stop =
(buffer#get_iter_at_mark stop)#compare where >= 0 &&
(buffer#get_iter_at_mark start)#compare where <= 0 in
let state_id = fst @@ self#find_id until in
let diff_opt = Interface.(match Coq.PrintOpt.(get diff) with
| StringValue diffs -> diffs
| _ -> "off") in
let proof_diff = Coq.proof_diff (diff_opt, state_id) in
Coq.bind proof_diff 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 =
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
let processed = Tags.Script.processed in
let unjustified = Tags.Script.unjustified in
let error_bg = Tags.Script.error_bg in
let error = Tags.Script.error in
let incomplete = Tags.Script.incomplete in
let all_tags = [
error_bg; to_process; incomplete; processed; unjustified; error ] in
let tags =
(if has_flag sentence `PROCESSING then [to_process]
else if has_flag sentence `ERROR then [error_bg]
else if has_flag sentence `INCOMPLETE then [incomplete]
else [processed]) @
(if has_flag sentence `UNSAFE then [unjustified] else [])
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 ?loc sentence text =
let start_sentence, stop_sentence, phrase = self#get_sentence sentence in
let pre_bytes, post_bytes = Option.cata Loc.unloc (0, String.length phrase) loc in
let pre = b2c phrase (pre_bytes - (sentence.byte_start)) in
let post = b2c phrase (post_bytes - (sentence.byte_start)) in
let start = start_sentence#forward_chars pre in
let stop = start_sentence#forward_chars post in
let markup = Glib.Markup.escape_text text in
buffer#apply_tag Tags.Script.tooltip ~start ~stop;
add_tooltip sentence start#offset stop#offset markup
method private debug_prompt ~tag msg =
match tag with
| "prompt" ->
messages#default_route#debug_prompt msg
| "goal" ->
forward_set_goals_of_dbg_session msg
| "init" -> forward_init_db ()
| _ ->
messages#default_route#push Debug msg
method set_debug_goal msg =
proof#set_debug_goal msg
method private process_feedback msg =
(* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt Xmlprotocol.(of_feedback Ppcmds msg)); *)
let pr_feedback msg =
let id = msg.span_id in
let sentence =
let finder _ state_id s =
match state_id, id with
| 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_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 msg_wo_sent mtype =
Minilib.log (mtype ^ " feedback message without a sentence") in
let unsupp_msg mtype =
if sentence <> None then
Minilib.log ("Unsupported feedback message " ^ mtype ^ " with a sentence")
in
let log ?id s = log_pp ?id (Pp.str s) in
begin match msg.contents, sentence with
| AddedAxiom, Some (id,sentence) ->
log ?id "AddedAxiom";
remove_flag sentence `PROCESSING;
remove_flag sentence `ERROR;
add_flag sentence `UNSAFE;
self#mark_as_needed sentence
| AddedAxiom, None -> msg_wo_sent "AddedAxiom"
| Processed, Some (id,sentence) ->
log ?id "Processed" ;
remove_flag sentence `PROCESSING;
self#mark_as_needed sentence;
forward_clear_db_highlight ()
| Processed, None -> msg_wo_sent "Processed"
| ProcessingIn _, Some (id,sentence) ->
log ?id "ProcessingIn";
add_flag sentence `PROCESSING;
self#mark_as_needed sentence
| ProcessingIn _, None -> msg_wo_sent "ProcessingIn"
| Incomplete, Some (id, sentence) ->
log ?id "Incomplete";
add_flag sentence `INCOMPLETE;
self#mark_as_needed sentence
| Incomplete, None -> msg_wo_sent "Incomplete"
| Complete, Some (id, sentence) ->
log ?id "Complete";
remove_flag sentence `INCOMPLETE;
self#mark_as_needed sentence
| Complete, None -> msg_wo_sent "Complete"
| GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) ->
log ?id "GlobRef";
self#attach_tooltip ~loc sentence
(Printf.sprintf "%s %s %s" filepath ident ty)
| GlobRef (_, _, _, _, _), None -> msg_wo_sent "GlobRef"
| Message(Error, loc, msg), Some (id,sentence) ->
log_pp ?id Pp.(str "ErrorMsg " ++ msg);
remove_flag sentence `PROCESSING;
let rmsg = Pp.string_of_ppcmds msg in
add_flag sentence (`ERROR (loc, rmsg));
self#mark_as_needed sentence;
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";
slaves_status <- CString.Map.add id status slaves_status
(* log unused feedback messages with a sentence *)
| GlobDef (_, _, _, _), _ -> unsupp_msg "GlobDef"
| FileDependency (_, _), _ -> unsupp_msg "FileDependency"
| FileLoaded (_, _), _ -> unsupp_msg "FileLoaded"
| Custom (_, _, _), _ -> unsupp_msg "Custom"
end
in
try match msg with
| MsgFeedback msg2 -> pr_feedback msg2
| MsgDebug (tag, msg2) ->
if tag = "prompt" then
Coq.set_stopped_in_debugger _ct true;
self#debug_prompt ~tag msg2
with e -> (Printf.printf "Exception: %s\n%!" (Printexc.to_string e);
flush stdout;
raise e)
method private commit_queue_transaction sentence =
(* A queued command has been successfully done, we push it to [cmd_stack].
We reget the iters here because Gtk is unable to warranty that they
were not modified meanwhile. Not really necessary but who knows... *)
self#mark_as_needed sentence;
let stop = buffer#get_iter_at_mark sentence.stop in
buffer#move_mark ~where:stop (`NAME "start_of_input");
method private apply_tag_in_sentence ?loc tag sentence =
let start, stop, phrase = self#get_sentence sentence in
match loc with
| None ->
buffer#apply_tag tag ~start ~stop
| Some loc ->
let start_bytes, stop_bytes = Loc.unloc loc in
let stop = start#forward_chars (b2c phrase (stop_bytes - (sentence.byte_start))) in
let start = start#forward_chars (b2c phrase (start_bytes - (sentence.byte_start))) in
buffer#apply_tag tag ~start ~stop
method private position_tag_at_sentence ?loc tag sentence =
self#apply_tag_in_sentence ?loc tag sentence
method private process_interp_error ?loc queue sentence msg tip id =
Coq.bind (Coq.return ()) (function () ->
let start, stop, _ = 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#apply_tag_in_sentence ?loc Tags.Script.error sentence;
buffer#place_cursor ~where:stop;
messages#default_route#clear;
messages#default_route#push Feedback.Error msg;
self#show_goals
end else
self#show_goals_aux ~move_insert:true ()
)
method private get_sentence sentence =
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
let phrase = start#get_slice ~stop in
start, stop, phrase
(** [fill_command_queue until q] fills a command queue until the [until]
condition returns true; it is fed with the number of phrases read and the
iters enclosing the current sentence. *)
method private fill_command_queue until queue =
let topstack =
if Doc.focused document then fst (Doc.context document) else [] in
let rec loop n iter prev_start =
(* prev_start is a workaround to avoid an endless loop. See #15873/#15984 *)
match Sentence.find buffer iter with
| None -> ()
| Some (start, stop) ->
if until n start stop then begin
()
end else if
List.exists (fun (_, s) ->
start#equal (buffer#get_iter_at_mark s.start) &&
stop#equal (buffer#get_iter_at_mark s.stop)) topstack
then begin
Queue.push (`Skip (start, stop)) queue;
loop n stop start#offset
end else begin
buffer#apply_tag Tags.Script.to_process ~start ~stop;
let sentence =
mk_sentence
~start:(`MARK (buffer#create_mark start))
~stop:(`MARK (buffer#create_mark stop))
[] in
Queue.push (`Sentence sentence) queue;
if start#offset <> prev_start && not stop#is_end then loop (succ n) stop start#offset
end
in
loop 0 self#get_start_of_input (-1)
method private discard_command_queue queue =
while not (Queue.is_empty queue) do
match Queue.pop queue with
| `Skip _ -> ()
| `Sentence sentence ->
let start = buffer#get_iter_at_mark sentence.start in
let stop = buffer#get_iter_at_mark sentence.stop in
buffer#remove_tag Tags.Script.to_process ~start ~stop;
buffer#delete_mark sentence.start;
buffer#delete_mark sentence.stop;
done
(** Compute the phrases until [until] returns [true]. *)
method private process_until ?move_insert until verbose =
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#default_route#clear;
script#set_editable false;
self#fill_command_queue until queue;
(* Now unlock and process asynchronously. Since [until]
may contain iterators, it shouldn't be used anymore *)
script#set_editable true;
Minilib.log "Begin command processing";
queue) in
let conclude topstack =
pop_info ();
script#recenter_insert;
match topstack with
| [] -> self#show_goals_aux ?move_insert ()
| (_,s)::_ -> self#backtrack_to_iter (buffer#get_iter_at_mark s.start) in
let process_queue queue =
let rec loop tip topstack =
if Queue.is_empty queue then conclude topstack else
match Queue.pop queue, topstack with
| `Skip(start,stop), [] ->
logger Feedback.Error (Pp.str "You must close the proof with Qed or Admitted");
self#discard_command_queue queue;
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));
loop tip topstack
| `Sentence sentence, _ :: _ -> assert false
| `Sentence ({ edit_id } as sentence), [] ->
add_flag sentence `PROCESSING;
Doc.push document sentence;
let start, _, phrase = self#get_sentence sentence in
(* script before last_offsets is not editable because Coq is processing *)
let s_offs = if start#offset > (snd last_offsets) then last_offsets else (0,0) in
let bp = c2b buffer s_offs start#offset in
sentence.byte_start <- bp;
let line_nb = start#line + 1 in
let bol_uni = start#offset - start#line_offset in
let bol_byte = c2b buffer s_offs bol_uni in
let bol_pos = bp - bol_byte in
last_offsets <- (bol_byte, bol_uni);
let coq_query = Coq.add ((((phrase,edit_id),(tip,verbose)),bp),(line_nb,bol_pos)) in
let handle_answer = function
| Good (id, Util.Inl (* NewTip *) ()) ->
Doc.assign_tip_id document id;
self#commit_queue_transaction sentence;
loop id []
| Good (id, Util.Inr (* Unfocus *) tip) ->
Doc.assign_tip_id document id;
let topstack, _ = Doc.context document in
self#exit_focus;
self#cleanup (Doc.cut_at document tip);
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 ?loc queue sentence msg tip id in
Coq.bind coq_query handle_answer
in
let tip =
try Doc.tip document
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#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
method stop_worker n =
Coq.bind (Coq.stop_worker n) (fun _ -> Coq.return ())
method get_slaves_status = processed, to_process, slaves_status
method get_n_errors =
Doc.fold_all document 0 (fun n _ _ s -> if has_flag s `ERROR then n+1 else n)
method get_errors =
let extract_error s =
match List.find (function `ERROR _ -> true | _ -> false) s.flags with
| `ERROR (loc, msg) ->
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
buffer#get_iter (`OFFSET (b2c phrase start))
end in iter#line + 1, msg
| _ -> assert false in
List.rev
(Doc.fold_all document [] (fun acc _ _ s ->
if has_flag s `ERROR then extract_error s :: acc else acc))
method process_next_phrase =
let until n _ _ = n >= 1 in
self#process_until ~move_insert:true until true
method process_db_cmd cmd ~next : unit Coq.task =
let db_cmd = Coq.db_cmd cmd in
Coq.bind db_cmd next
method process_db_configd cmd ~next : unit Coq.task =
let db_configd = Coq.db_configd cmd in
Coq.bind db_configd next
method process_db_upd_bpts updates ~next : unit Coq.task =
let db_upd_bpts = Coq.db_upd_bpts updates in
Coq.bind db_upd_bpts next
method process_db_continue opt ~next : unit Coq.task =
let db_continue = Coq.db_continue opt in
Coq.bind db_continue next
method process_db_stack ~next : unit Coq.task =
let db_stack = Coq.db_stack () in
Coq.bind db_stack next
method process_db_vars framenum ~next : unit Coq.task =
let db_vars = Coq.db_vars framenum in
Coq.bind db_vars next
method private process_until_iter iter =
let until _ start stop =
if Preferences.stop_before#get then stop#compare iter > 0
else start#compare iter >= 0
in
self#process_until until false
method process_until_end_or_error =
self#process_until_iter self#get_end_of_input
(* finds the state_id and if it an unfocus is needed to reach it *)
method private find_id until =
try
Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
with Not_found -> initial_state, Doc.focused document
method private cleanup seg =
if seg <> [] then begin
let start = buffer#get_iter_at_mark (CList.last seg).start in
let stop = buffer#get_iter_at_mark (CList.hd seg).stop in
Minilib.log
(Printf.sprintf "Cleanup in range %d -> %d" start#offset stop#offset);
buffer#remove_tag Tags.Script.processed ~start ~stop;
buffer#remove_tag Tags.Script.incomplete ~start ~stop;
buffer#remove_tag Tags.Script.unjustified ~start ~stop;
buffer#remove_tag Tags.Script.tooltip ~start ~stop;
buffer#remove_tag Tags.Script.to_process ~start ~stop;
buffer#move_mark ~where:start (`NAME "start_of_input")
end;
List.iter (fun { start } -> buffer#delete_mark start) seg;
List.iter (fun { stop } -> buffer#delete_mark stop) seg;
self#print_stack
(** Wrapper around the raw undo command *)
method private backtrack_to_id ?(move_insert=true) (to_id, unfocus_needed) =
Minilib.log("backtrack_to_id "^Stateid.to_string to_id^
" (unfocus_needed="^string_of_bool unfocus_needed^")");
let opening () =
push_info "Coq is undoing" in
let conclusion () =
pop_info ();
if move_insert then begin
buffer#place_cursor ~where:self#get_start_of_input;
script#recenter_insert;
end;
let start = self#get_start_of_input in
let stop = self#get_end_of_input in
Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);
buffer#remove_tag Tags.Script.tooltip ~start ~stop;
buffer#remove_tag Tags.Script.processed ~start ~stop;
buffer#remove_tag Tags.Script.incomplete ~start ~stop;
buffer#remove_tag Tags.Script.to_process ~start ~stop;
buffer#remove_tag Tags.Script.unjustified ~start ~stop;
self#show_goals in
Coq.bind (Coq.lift opening) (fun () ->
let rec undo to_id unfocus_needed =
Coq.bind (Coq.edit_at to_id) (function
| Good (CSig.Inl (* NewTip *) ()) ->
if unfocus_needed then self#exit_focus;
self#cleanup (Doc.cut_at document to_id);
conclusion ()
| Good (CSig.Inr (* Focus *) (stop_id,(start_id,tip))) ->
if unfocus_needed then self#exit_focus;
self#cleanup (Doc.cut_at document tip);
self#enter_focus start_id stop_id;
self#cleanup (Doc.cut_at document to_id);
conclusion ()
| Fail (safe_id, loc, msg) ->
(* if loc <> None then messages#push Feedback.Error (Richpp.richpp_of_string "Fixme LOC"); *)
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))
in
undo to_id unfocus_needed)
method backtrack_to_begin =
let until (id : Doc.id option) _ stop = (id = (Some (Stateid.of_int 1))) in
fun () -> self#backtrack_to_id ~move_insert:false (self#find_id until)
method private backtrack_until ?move_insert until =
self#backtrack_to_id ?move_insert (self#find_id until)
method private backtrack_to_iter ?move_insert iter =
let until _ _ stop = iter#compare (buffer#get_iter_at_mark stop) >= 0 in
self#backtrack_until ?move_insert until
method private handle_failure_aux
?(move_insert=false) (safe_id, (loc : (int * int) option), msg)
=
messages#default_route#push Feedback.Error msg;
if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ())
else
Coq.seq
(self#backtrack_until ~move_insert
(fun id _ _ -> id = Some safe_id))
(Coq.lift (fun () -> script#recenter_insert))
method handle_failure f = self#handle_failure_aux f
method backtrack_last_phrase =
messages#default_route#clear;
try
let tgt = Doc.before_tip document in
self#backtrack_to_id tgt
with Not_found -> Coq.return (Coq.reset_coqtop _ct)
method go_to_insert =
Coq.bind (Coq.return ()) (fun () ->
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
else self#backtrack_to_iter ~move_insert:false point)
method go_to_mark m =
Coq.bind (Coq.return ()) (fun () ->
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)
(Coq.lift (fun () -> Sentence.tag_on_insert buffer))
else Coq.seq (self#backtrack_to_iter ~move_insert:false point)
(Coq.lift (fun () -> Sentence.tag_on_insert buffer)))
method handle_reset_initial =
let action () =
(* clear the stack *)
if Doc.focused document then Doc.unfocus document;
while not (Doc.is_empty document) do
let phrase = Doc.pop document in
buffer#delete_mark phrase.start;
buffer#delete_mark phrase.stop
done;
List.iter
(buffer#remove_tag ~start:buffer#start_iter ~stop:buffer#end_iter)
Tags.Script.all_but_bpt;
(* reset the buffer *)
buffer#move_mark ~where:buffer#start_iter (`NAME "start_of_input");
buffer#move_mark ~where:buffer#end_iter (`NAME "stop_of_input");
Sentence.tag_all buffer;
(* clear the views *)
messages#default_route#clear;
proof#clear ();
clear_info ();
processed <- 0;
to_process <- 0;
push_info "Restarted";
(* apply the initial commands to coq *)
in
Coq.seq (Coq.lift action) self#initialize
method initialize =
let get_initial_state =
let next = function
| Fail (_, _, message) ->
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
Coq.bind (Coq.init (get_filename ())) next in
Coq.seq get_initial_state Coq.PrintOpt.enforce
end
|