let tac ast _ =
if (MatitaScript.current ())#onGoingProof () then
(MatitaScript.current ())#advance
- ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast)))
+ ~statement:("\n"
+ ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast)))
()
in
let tac_w_term ast _ =
if (MatitaScript.current ())#onGoingProof () then
let buf = source_buffer in
buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
- ("\n" ^ GrafiteAstPp.pp_tactic ast)
+ ("\n"
+ ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:CicNotationPp.pp_term ast)
in
let tbar = main in
connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
(** selections / clipboards handling *)
- method private markup_selected = MatitaMathView.has_selection ()
- method private text_selected =
+ method markupSelected = MatitaMathView.has_selection ()
+ method private textSelected =
(source_buffer#get_iter_at_mark `INSERT)#compare
(source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
- method private something_selected =
- self#markup_selected || self#text_selected
- method private markup_stored = MatitaMathView.has_clipboard ()
- method private text_stored = clipboard#text <> None
- method private something_stored = self#markup_stored || self#text_stored
+ method private somethingSelected = self#markupSelected || self#textSelected
+ method private markupStored = MatitaMathView.has_clipboard ()
+ method private textStored = clipboard#text <> None
+ method private somethingStored = self#markupStored || self#textStored
- method canCopy = self#something_selected
- method canCut = self#text_selected
- method canDelete = self#text_selected
- method canPaste = self#something_stored
- method canPastePattern = self#markup_stored
+ method canCopy = self#somethingSelected
+ method canCut = self#textSelected
+ method canDelete = self#textSelected
+ method canPaste = self#somethingStored
+ method canPastePattern = self#markupStored
method copy () =
- if self#text_selected
+ if self#textSelected
then begin
MatitaMathView.empty_clipboard ();
source_view#buffer#copy_clipboard clipboard;