- let module A = TacticAst in
- let hole = CicAst.UserInput in
- let tac ast _ =
- let ast = A.Tactic ast in
- ignore (interpreter#evalAst ast);
- ignore (script#advance ast)
- in
- let tac_w_term ast _ =
-(* gui#console#clear (); *)
- gui#console#show ~msg:(TacticAstPp.pp_tactic ast) ();
- gui#main#mainWin#present ()
+ (* 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 =
+ 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
+ ()
+
+ (* math viewers *)
+let _ =
+ let sequent_viewer = MatitaMathView.sequentViewer_instance () in
+ let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
+ sequent_viewer#set_href_callback
+ (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri (UriManager.uri_of_string uri))));
+ let browser_observer _ = MatitaMathView.refresh_all_browsers () in
+ let sequents_observer status =
+ sequents_viewer#reset;
+ match status.proof_status with
+ | Incomplete_proof ((proof, goal) as status) ->
+ sequents_viewer#load_sequents status;
+ sequents_viewer#goto_sequent goal
+ | Proof proof ->
+ prerr_endline "sequents_viewer#load_logo_with_qed (no proof)"; ()
+ | No_proof ->
+ prerr_endline "sequents_viewer#load_logo (no proof)"; ()
+ | Intermediate _ ->
+ assert false (* only the engine may be in this state *)