+let currentProof = MatitaProof.instance ()
+
+let sequent_viewer = MatitaMathView.sequent_viewer_instance ()
+let sequents_viewer = MatitaMathView.sequents_viewer_instance ()
+let _ = (* attach observers to proof status *)
+ let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in
+ let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
+ sequents_viewer#reset;
+ (match goal_opt with
+ | None -> ()
+ | Some goal ->
+ sequents_viewer#load_sequents metasenv;
+ sequents_viewer#goto_sequent goal)
+ in
+ currentProof#addObserver sequents_observer;
+ currentProof#addObserver browser_observer;
+ currentProof#connect `Quit (fun () ->
+ (* quit program, asking for confirmation if needed *)
+ if not (currentProof#onGoing ()) ||
+ (ask_confirmation ~gui
+ ~msg:("Proof in progress, are you sure you want to quit?") ())
+ then
+ GMain.Main.quit ();
+ false);
+ currentProof#connect `Abort (fun () -> sequents_viewer#reset; false)
+
+let interpreter =
+ let mathViewer = MatitaMathView.mathViewer () in
+ MatitaInterpreter.interpreter ~console:gui#console ~mathViewer ()
+let script = MatitaScript.script ~interpreter
+let _ =
+ let href_callback uri =
+ let term = CicAst.Uri (uri, None) in
+ ignore (interpreter#evalAst (TacticAst.Command (TacticAst.Check term)))
+ in
+ sequent_viewer#set_href_callback (Some href_callback)
+
+let console_callback s =
+ let module A = TacticAst in
+ let rec strip_locations = function
+ | A.LocatedTactical (loc, tac) -> strip_locations tac
+ | tac -> tac
+ in
+ let needed_by_script ast =
+ match strip_locations ast with
+ | A.Tactic _
+ | A.Command
+ (A.Inductive _ | A.Theorem _ | A.Coercion _ | A.Qed _ | A.Proof) ->
+ true
+ | _ -> false
+ in
+ let ast = disambiguator#parserr#parseTactical (Stream.of_string s) in
+ debug_print (sprintf "evaluating '%s'" s);
+ if needed_by_script ast then
+ script#advance s
+ else
+ interpreter#evalAst ast