diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-02 21:32:26 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-04 11:13:49 +0200 |
| commit | 8bcf71360261d789ac3ab919bc49309df678628f (patch) | |
| tree | 0bf128027766f3113e2b19686c1a065088ceb3fa /ide | |
| parent | 1fe73e6af81759fa8b78c8660745492ed886d477 (diff) | |
labelizing arguments
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/wg_ProofView.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 60b2d9e60..0bf5afbfd 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -47,7 +47,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 unfoc_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 = @@ -65,7 +65,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals unfoc_goals hints = matc let head_str = Printf.sprintf "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "") in - let goal_str shownum index total = + let goal_str ?(shownum=false) index total = if shownum then Printf.sprintf "______________________________________(%d/%d)\n" index total else Printf.sprintf @@ -100,17 +100,17 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals unfoc_goals hints = matc [tag] else [] in - proof#buffer#insert (goal_str true 1 goals_cnt); + proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt); insert_xml proof#buffer (Richpp.richpp_of_pp width cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) - let fold_goal shownum i _ { Interface.goal_ccl = g } = - proof#buffer#insert (goal_str shownum i goals_cnt); + 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 true) 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 @@ -120,7 +120,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals unfoc_goals hints = matc if unfoc<>[] then begin proof#buffer#insert "\nUnfocused Goals:\n"; - Util.List.fold_left_i (fold_goal false) 0 () unfoc + Util.List.fold_left_i (fold_goal ~shownum:false) 0 () unfoc end end; ignore(proof#buffer#place_cursor @@ -187,7 +187,7 @@ let display mode (view : #GText.view_skel) goals hints evars = List.iteri iter bg end | Some { Interface.fg_goals = fg; bg_goals = bg } -> - mode view fg bg hints + mode view fg ~unfoc_goals:bg hints let proof_view () = |