aboutsummaryrefslogtreecommitdiff
path: root/ide/coqide/wg_ProofView.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide/wg_ProofView.ml')
-rw-r--r--ide/coqide/wg_ProofView.ml252
1 files changed, 252 insertions, 0 deletions
diff --git a/ide/coqide/wg_ProofView.ml b/ide/coqide/wg_ProofView.ml
new file mode 100644
index 0000000000..1de63953af
--- /dev/null
+++ b/ide/coqide/wg_ProofView.ml
@@ -0,0 +1,252 @@
+(************************************************************************)
+(* * 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 Preferences
+open Ideutils
+
+class type proof_view =
+ object
+ inherit GObj.widget
+ method source_buffer : GSourceView3.source_buffer
+ method buffer : GText.buffer
+ method refresh : force:bool -> unit
+ method clear : unit -> unit
+ method set_goals : Interface.goals option -> unit
+ method set_evars : Interface.evar list option -> unit
+ end
+
+(* tag is the tag to be hooked, item is the item covered by this tag, make_menu
+ * * is the template for building menu if needed, sel_cb is the callback if
+ * there
+ * * is a selection o said menu, hover_cb is the callback when there is only
+ * * hovering *)
+let hook_tag_cb tag menu_content sel_cb hover_cb =
+ ignore (tag#connect#event ~callback:
+ (fun ~origin evt it ->
+ let iter = new GText.iter it in
+ let start = iter#backward_to_tag_toggle (Some tag) in
+ let stop = iter#forward_to_tag_toggle (Some tag) in
+ match GdkEvent.get_type evt with
+ | `BUTTON_PRESS ->
+ let ev = GdkEvent.Button.cast evt in
+ if (GdkEvent.Button.button ev) <> 3 then false else begin
+ let ctxt_menu = GMenu.menu () in
+ let factory = new GMenu.factory ctxt_menu in
+ List.iter
+ (fun (text,cmd) -> ignore (factory#add_item text ~callback:(sel_cb cmd)))
+ menu_content;
+ ctxt_menu#popup ~button:3 ~time:(GdkEvent.Button.time ev);
+ true
+ end
+ | `MOTION_NOTIFY ->
+ hover_cb start stop; false
+ | _ -> false))
+
+let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = match goals with
+ | [] -> assert false
+ | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: rem_goals ->
+ let on_hover sel_start sel_stop =
+ proof#buffer#remove_tag
+ ~start:proof#buffer#start_iter
+ ~stop:sel_start
+ Tags.Proof.highlight;
+ proof#buffer#remove_tag
+ ~start:sel_stop
+ ~stop:proof#buffer#end_iter
+ Tags.Proof.highlight;
+ proof#buffer#apply_tag ~start:sel_start ~stop:sel_stop Tags.Proof.highlight
+ in
+ let goals_cnt = List.length rem_goals + 1 in
+ let head_str = Printf.sprintf
+ "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "")
+ in
+ let goal_str ?(shownum=false) index total =
+ if shownum then Printf.sprintf
+ "______________________________________(%d/%d)\n" index total
+ else Printf.sprintf
+ "______________________________________\n"
+ in
+ (* Insert current goal and its hypotheses *)
+ let hyps_hints, goal_hints = match hints with
+ | None -> [], []
+ | Some (hl, h) -> (hl, h)
+ in
+ let width = Ideutils.textview_width proof in
+ let rec insert_hyp hints hs = match hs with
+ | [] -> ()
+ | hyp :: hs ->
+ let tags, rem_hints = match hints with
+ | [] -> [], []
+ | hint :: hints ->
+ let tag = proof#buffer#create_tag [] in
+ let () = hook_tag_cb tag hint sel_cb on_hover in
+ [tag], hints
+ in
+ let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp width hyp) in
+ proof#buffer#insert "\n";
+ insert_hyp rem_hints hs
+ in
+ let () = proof#buffer#insert head_str in
+ let () = insert_hyp hyps_hints hyps in
+ let () =
+ let _ = if goal_hints <> [] then
+ let tag = proof#buffer#create_tag [] in
+ let () = hook_tag_cb tag goal_hints sel_cb on_hover in
+ [tag]
+ else []
+ in
+ proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt);
+ insert_xml ~tags:[Tags.Proof.goal] proof#buffer (Richpp.richpp_of_pp width cur_goal);
+ proof#buffer#insert "\n"
+ in
+ (* Insert remaining goals (no hypotheses) *)
+ let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g } =
+ proof#buffer#insert (goal_str ~shownum i goals_cnt);
+ insert_xml proof#buffer (Richpp.richpp_of_pp width g);
+ proof#buffer#insert "\n"
+ in
+ let () = Util.List.fold_left_i (fold_goal ~shownum:true) 2 () rem_goals in
+ (* show unfocused goal if option set *)
+ (* Insert remaining goals (no hypotheses) *)
+ if Coq.PrintOpt.printing_unfocused () then
+ begin
+ ignore(proof#buffer#place_cursor ~where:(proof#buffer#end_iter));
+ let unfoc = List.flatten (List.rev (List.map (fun (x,y) -> x@y) unfoc_goals)) in
+ if unfoc<>[] then
+ begin
+ proof#buffer#insert "\nUnfocused Goals:\n";
+ Util.List.fold_left_i (fold_goal ~shownum:false) 0 () unfoc
+ end
+ end;
+ ignore(proof#buffer#place_cursor
+ ~where:(proof#buffer#end_iter#backward_to_tag_toggle
+ (Some Tags.Proof.goal)));
+ ignore(proof#scroll_to_mark `INSERT)
+
+let rec flatten = function
+| [] -> []
+| (lg, rg) :: l ->
+ let inner = flatten l in
+ List.rev_append lg inner @ rg
+
+let display mode (view : #GText.view_skel) goals hints evars =
+ let () = view#buffer#set_text "" in
+ let width = Ideutils.textview_width view in
+ match goals with
+ | None -> ()
+ (* No proof in progress *)
+ | Some { Interface.fg_goals = []; bg_goals = bg; shelved_goals; given_up_goals; } ->
+ let bg = flatten (List.rev bg) in
+ let evars = match evars with None -> [] | Some evs -> evs in
+ begin match (bg, shelved_goals,given_up_goals, evars) with
+ | [], [], [], [] ->
+ view#buffer#insert "No more subgoals."
+ | [], [], [], _ :: _ ->
+ (* A proof has been finished, but not concluded *)
+ view#buffer#insert "No more subgoals, but there are non-instantiated existential variables:\n\n";
+ let iter evar =
+ let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
+ view#buffer#insert msg
+ in
+ List.iter iter evars;
+ view#buffer#insert "\nYou can use Grab Existential Variables."
+ | [], [], _, _ ->
+ (* The proof is finished, with the exception of given up goals. *)
+ view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
+ let iter goal =
+ insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
+ view#buffer#insert "\n"
+ in
+ List.iter iter given_up_goals;
+ view#buffer#insert "\nYou need to go back and solve them."
+ | [], _, _, _ ->
+ (* All the goals have been resolved but those on the shelf. *)
+ view#buffer#insert "All the remaining goals are on the shelf:\n\n";
+ let iter goal =
+ insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
+ view#buffer#insert "\n"
+ in
+ List.iter iter shelved_goals
+ | _, _, _, _ ->
+ (* No foreground proofs, but still unfocused ones *)
+ let total = List.length bg in
+ let goal_str index = Printf.sprintf
+ "______________________________________(%d/%d)\n" index total
+ in
+ view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
+ let iter i goal =
+ let () = view#buffer#insert (goal_str (succ i)) in
+ insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
+ view#buffer#insert "\n"
+ in
+ List.iteri iter bg
+ end
+ | Some { Interface.fg_goals = fg; bg_goals = bg } ->
+ mode view fg ~unfoc_goals:bg hints
+
+
+let proof_view () =
+ let buffer = GSourceView3.source_buffer
+ ~highlight_matching_brackets:true
+ ~tag_table:Tags.Proof.table
+ ?style_scheme:(style_manager#style_scheme source_style#get) ()
+ in
+ let text_buffer = new GText.buffer buffer#as_buffer in
+ let view = GSourceView3.source_view
+ ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD ()
+ in
+ let () = Gtk_parsing.fix_double_click view in
+ let default_clipboard = GData.clipboard Gdk.Atom.primary in
+ let _ = buffer#add_selection_clipboard default_clipboard in
+(* FIXME: handle this using CSS *)
+(* let cb clr = view#misc#modify_bg [`NORMAL, `NAME clr] in *)
+(* let _ = background_color#connect#changed ~callback:cb in *)
+(* let _ = view#misc#connect#realize ~callback:(fun () -> cb background_color#get) in *)
+ let cb ft = view#misc#modify_font (GPango.font_description_from_string ft) in
+ stick text_font view cb;
+
+ let pf = object
+ inherit GObj.widget view#as_widget
+ val mutable goals = None
+ val mutable evars = None
+ val mutable last_width = -1
+
+ method source_buffer = buffer
+
+ method buffer = text_buffer
+
+ method clear () = buffer#set_text ""
+
+ method set_goals gls = goals <- gls
+
+ method set_evars evs = evars <- evs
+
+ method refresh ~force =
+ (* We need to block updates here due to the following race:
+ insertion of messages may create a vertical scrollbar, this
+ will trigger a width change, calling refresh again and
+ going into an infinite loop. *)
+ let width = Ideutils.textview_width view in
+ (* Could still this method race if the scrollbar changes the
+ textview_width ?? *)
+ let needed = force || last_width <> width in
+ if needed then begin
+ last_width <- width;
+ let dummy _ () = () in
+ display (mode_tactic dummy) view goals None evars
+ end
+ end
+ in
+ (* Is there a better way to connect the signal ? *)
+ (* Can this be done in the object constructor? *)
+ let w_cb _ = pf#refresh ~force:false in
+ ignore (view#misc#connect#size_allocate ~callback:w_cb);
+ pf
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:47:54 +0000