summaryrefslogtreecommitdiff
path: root/ide/wg_ProofView.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/wg_ProofView.ml')
-rw-r--r--ide/wg_ProofView.ml98
1 files changed, 65 insertions, 33 deletions
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 47c86045..9be562d3 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * 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 *)
+(* // * 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
@@ -14,11 +16,10 @@ class type proof_view =
object
inherit GObj.widget
method buffer : GText.buffer
- method refresh : unit -> unit
+ method refresh : force:bool -> unit
method clear : unit -> unit
method set_goals : Interface.goals option -> unit
method set_evars : Interface.evar list option -> unit
- method width : int
end
(* tag is the tag to be hooked, item is the item covered by this tag, make_menu
@@ -48,7 +49,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb =
hover_cb start stop; false
| _ -> false))
-let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
+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 =
@@ -66,14 +67,18 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
let head_str = Printf.sprintf
"%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "")
in
- let goal_str index total = Printf.sprintf
- "______________________________________(%d/%d)\n" index total
+ 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 ->
@@ -84,7 +89,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
let () = hook_tag_cb tag hint sel_cb on_hover in
[tag], hints
in
- let () = insert_xml ~tags proof#buffer hyp in
+ let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp width hyp) in
proof#buffer#insert "\n";
insert_hyp rem_hints hs
in
@@ -97,22 +102,33 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
[tag]
else []
in
- proof#buffer#insert (goal_str 1 goals_cnt);
- insert_xml proof#buffer cur_goal;
+ 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 i _ { Interface.goal_ccl = g } =
- proof#buffer#insert (goal_str i goals_cnt);
- insert_xml proof#buffer g;
+ 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 2 () rem_goals 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 ~use_align:true ~yalign:0.95 `INSERT)
+ ignore(proof#scroll_to_mark `INSERT)
let rec flatten = function
| [] -> []
@@ -122,6 +138,7 @@ let rec flatten = function
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 *)
@@ -144,7 +161,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
(* 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 goal.Interface.goal_ccl;
+ insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
view#buffer#insert "\n"
in
List.iter iter given_up_goals;
@@ -153,7 +170,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
(* 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 goal.Interface.goal_ccl;
+ insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl);
view#buffer#insert "\n"
in
List.iter iter shelved_goals
@@ -166,13 +183,14 @@ let display mode (view : #GText.view_skel) goals hints evars =
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 goal.Interface.goal_ccl;
+ 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 } ->
- mode view fg hints
+ | Some { Interface.fg_goals = fg; bg_goals = bg } ->
+ mode view fg ~unfoc_goals:bg hints
+
let proof_view () =
let buffer = GSourceView2.source_buffer
@@ -187,15 +205,16 @@ let proof_view () =
let default_clipboard = GData.clipboard Gdk.Atom.primary in
let _ = buffer#add_selection_clipboard default_clipboard in
let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in
- let _ = background_color#connect#changed cb in
- let _ = view#misc#connect#realize (fun () -> cb background_color#get) 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 (Pango.Font.from_string ft) in
stick text_font view cb;
- object
+ let pf = object
inherit GObj.widget view#as_widget
val mutable goals = None
val mutable evars = None
+ val mutable last_width = -1
method buffer = text_buffer
@@ -205,11 +224,24 @@ let proof_view () =
method set_evars evs = evars <- evs
- method refresh () =
- let dummy _ () = () in
- display (mode_tactic dummy) (view :> GText.view_skel) goals None evars
-
- method width = Ideutils.textview_width (view :> GText.view_skel)
+ 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
-
-(* ignore (proof_buffer#add_selection_clipboard cb); *)
+ 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.39.1) at 2024-05-07 05:04:07 +0000