- let currentProof = (currentProof :> MatitaTypes.currentProof) in
- ignore (MatitaMathView.cicBrowser ~disambiguator ~currentProof ())));
- connect_button gui#script#scriptWinForwardButton script_forward;
- connect_button gui#script#scriptWinBackButton script_back;
- connect_button gui#script#scriptWinJumpButton script_jump;
- let module A = TacticAst in
- let hole = CicAst.UserInput in
- let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in
- let tac_w_term ast _ =
-(* gui#console#clear (); *)
- gui#console#show ~msg:(TacticAstPp.pp_tactic ast) ();
- gui#main#mainWin#present ()
+ ignore (MatitaMathView.cicBrowser ())));
+ (* font sizes *)
+ ignore (gui#main#increaseFontSizeMenuItem#connect#activate (fun _ ->
+ gui#increaseFontSize ();
+ MatitaMathView.increase_font_size ();
+ MatitaMathView.update_font_sizes ()));
+ ignore (gui#main#decreaseFontSizeMenuItem#connect#activate (fun _ ->
+ gui#decreaseFontSize ();
+ MatitaMathView.decrease_font_size ();
+ MatitaMathView.update_font_sizes ()));
+ ignore (gui#main#normalFontSizeMenuItem#connect#activate (fun _ ->
+ gui#resetFontSize ();
+ MatitaMathView.reset_font_size ();
+ MatitaMathView.update_font_sizes ()));
+ MatitaMathView.reset_font_size ();
+ (* disambiguator callback *)
+ MatitaDisambiguator.set_choose_uris_callback
+ (MatitaGui.interactive_uri_choice ());
+ MatitaDisambiguator.set_choose_interp_callback
+ (MatitaGui.interactive_interp_choice ())
+
+let script =
+ let s =
+ MatitaScript.script
+ ~view:(gui#sourceView :> GText.view)
+ ~init:(Lazy.force MatitaEngine.initial_status)
+ ~mathviewer:(MatitaMathView.mathViewer ())
+ ~urichooser:(fun uris ->
+ try
+ MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
+ ~title:"Matita: URI chooser"
+ ~msg:"Select the URI" ~hide_uri_entry:true
+ ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
+ ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
+ () ~id:"boh?" uris
+ with MatitaTypes.Cancel -> [])
+ ~set_star:gui#setStar
+ ~ask_confirmation:
+ (fun ~title ~message ->
+ MatitaGtkMisc.ask_confirmation ~title ~message
+ ~parent:gui#main#toplevel ())
+ ~develcreator:gui#createDevelopment
+ ()