false);
currentProof#connect `Abort (fun () -> sequents_viewer#reset; false)
+let mathViewer = MatitaMathView.mathViewer ()
+let cicBrowser = MatitaMathView.cicBrowser ()
let interpreter =
let console = (gui#console :> MatitaTypes.console) in
let currentProof = (currentProof :> MatitaTypes.currentProof) in
new MatitaInterpreter.interpreter
- ~disambiguator ~currentProof ~console ~dbd ()
+ ~disambiguator ~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)
(** {2 Script window handling} *)
let i = ref 0 in
List.iter
(fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t)))
- sequent_viewer#get_selected_terms)
+ sequent_viewer#get_selected_terms);
+ addDebugItem "show cic browser" (fun () -> gui#browser#browserWin#show ());
end
(** </DEBUGGING> *)
(try
load_script Sys.argv.(1)
with Invalid_argument _ -> ());
+ gui#console#show ();
GtkThread.main ()