let currentProof = new MatitaProof.currentProof
-let proof_viewer = MatitaMathView.proof_viewer_instance ()
let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
let sequents_viewer =
let set_goal goal =
MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
~sequent_viewer ~set_goal ()
let _ = (* attach observers to proof status *)
- let proof_observer _ (status, ()) =
- let ((uri_opt, _, _, _), _) = status in
- proof_viewer#load_proof status;
- in
+ let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in
let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
sequents_viewer#reset;
(match goal_opt with
sequents_viewer#goto_sequent goal)
in
currentProof#addObserver sequents_observer;
- currentProof#addObserver proof_observer;
+ currentProof#addObserver browser_observer;
currentProof#connect `Quit (fun () ->
(* quit program, asking for confirmation if needed *)
if not (currentProof#onGoing ()) ||
false);
currentProof#connect `Abort (fun () -> sequents_viewer#reset; false)
-let mathViewer = MatitaMathView.mathViewer ()
-let cicBrowser = MatitaMathView.cicBrowser ()
+let currentProof = (currentProof :> MatitaTypes.currentProof)
+let mathViewer =
+ MatitaMathView.mathViewer ~disambiguator
+ ~currentProof:(currentProof :> MatitaTypes.currentProof) ()
let interpreter =
let console = (gui#console :> MatitaTypes.console) in
- let currentProof = (currentProof :> MatitaTypes.currentProof) in
new MatitaInterpreter.interpreter
- ~disambiguator ~currentProof ~console ~mathViewer ~dbd ()
+ ~disambiguator ~currentProof:(currentProof :> MatitaTypes.currentProof)
+ ~console ~mathViewer ~dbd ()
let _ =
let href_callback uri =
let term = CicAst.Uri (UriManager.string_of_uri uri, None) in
ignore (interpreter#evalAst (TacticAst.Command (TacticAst.Check term)))
in
- proof_viewer#set_href_callback (Some href_callback);
- sequent_viewer#set_href_callback (Some href_callback);
- mathViewer#set_href_callback (Some href_callback)
+ sequent_viewer#set_href_callback (Some href_callback)
(** {2 Script window handling} *)
gui#console#echo_error (sprintf
"Don't know what to do with file: %s\nUnrecognized file format."
f)));
+ ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
+ 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 hole = CicAst.UserInput in
let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in
let tac_w_term ast _ =
- gui#console#clear ();
+(* gui#console#clear (); *)
gui#console#show ~msg:(TacticAstPp.pp_tactic ast) ();
gui#main#mainWin#present ()
in
List.iter
(fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t)))
sequent_viewer#get_selected_terms);
- addDebugItem "show cic browser" (fun () -> gui#browser#browserWin#show ());
+ addDebugItem "refresh all browsers" MatitaMathView.refresh_all_browsers;
end
(** </DEBUGGING> *)