diff options
Diffstat (limited to 'ide/wg_ProofView.ml')
| -rw-r--r-- | ide/wg_ProofView.ml | 41 |
1 files changed, 20 insertions, 21 deletions
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 0007203e..47c86045 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -7,6 +7,8 @@ (************************************************************************) open Util +open Preferences +open Ideutils class type proof_view = object @@ -82,26 +84,28 @@ 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 () = proof#buffer#insert ~tags (hyp ^ "\n") in + let () = insert_xml ~tags proof#buffer 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 tags = Tags.Proof.goal :: if goal_hints <> [] then + 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 1 goals_cnt); - proof#buffer#insert ~tags cur_goal; + insert_xml proof#buffer 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); - proof#buffer#insert (g ^ "\n") + insert_xml proof#buffer g; + proof#buffer#insert "\n" in let () = Util.List.fold_left_i fold_goal 2 () rem_goals in @@ -110,17 +114,6 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with (Some Tags.Proof.goal))); ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT) -let mode_cesar (proof : #GText.view_skel) = function - | [] -> assert false - | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ -> - proof#buffer#insert " *** Declarative Mode ***\n"; - List.iter - (fun hyp -> proof#buffer#insert (hyp^"\n")) - hyps; - proof#buffer#insert "______________________________________\n"; - proof#buffer#insert ("thesis := \n "^cur_goal^"\n"); - ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT)) - let rec flatten = function | [] -> [] | (lg, rg) :: l -> @@ -151,8 +144,8 @@ 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 = - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg + insert_xml view#buffer 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." @@ -160,8 +153,8 @@ 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 = - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg + insert_xml view#buffer goal.Interface.goal_ccl; + view#buffer#insert "\n" in List.iter iter shelved_goals | _, _, _, _ -> @@ -173,8 +166,8 @@ 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 - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg + insert_xml view#buffer goal.Interface.goal_ccl; + view#buffer#insert "\n" in List.iteri iter bg end @@ -193,6 +186,12 @@ let proof_view () = 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 + 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 cb ft = view#misc#modify_font (Pango.Font.from_string ft) in + stick text_font view cb; + object inherit GObj.widget view#as_widget val mutable goals = None |