~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")
()
-let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner")
+
+let owner = (Helm_registry.get "matita.owner") ;;
+let _ = MetadataTypes.ownerize_tables owner ;;
+let _ = MatitaDb.clean_owner_environment dbd owner ;;
+let _ = MatitaDb.create_owner_environment dbd owner ;;
+
let gui = MatitaGui.instance ()
let disambiguator =
new MatitaDisambiguator.disambiguator ~parserr ~dbd
~chooseInterp:(interactive_interp_choice ~gui)
()
-let currentProof = new MatitaProof.currentProof
+let currentProof = MatitaProof.instance ()
+
-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 mathViewer = MatitaMathView.mathViewer ~disambiguator ()
let interpreter =
- let console = (gui#console :> MatitaTypes.console) in
- let currentProof = (currentProof :> MatitaTypes.currentProof) in
- new MatitaInterpreter.interpreter
- ~disambiguator ~currentProof ~console ~mathViewer ~dbd ()
+ let console = gui#console in
+ MatitaInterpreter.interpreter ~disambiguator ~console ~mathViewer ()
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 _ ->
+ ignore (MatitaMathView.cicBrowser ~disambiguator ())));
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> *)
let _ =
(* CicEnvironment.set_trust (fun _ -> false); *)
+(*
(try
load_script Sys.argv.(1)
with Invalid_argument _ -> ());
- gui#console#show ();
+*)
+ if Pcre.pmatch ~pat:"cicbrowser$" Sys.argv.(0) then begin (* cicbrowser *)
+ let browser = MatitaMathView.cicBrowser ~disambiguator () in
+ Helm_registry.set "matita.mode" "cicbrowser";
+ try
+ browser#loadUri Sys.argv.(1)
+ with Invalid_argument _ -> ()
+ end else begin (* matita *)
+ Helm_registry.set "matita.mode" "matita";
+ gui#main#mainWin#show ();
+ gui#toolbar#toolBarWin#show ();
+ gui#console#show ()
+ end;
GtkThread.main ()