+let parserr = new MatitaDisambiguator.parserr ()
+let mqiconn = MQIConn.init ()
+let disambiguator =
+ new MatitaDisambiguator.disambiguator ~parserr ~mqiconn
+ ~chooseUris:(interactive_user_uri_choice ~gui)
+ ~chooseInterp:(interactive_interp_choice ~gui)
+ ()
+let new_proof proof =
+ (* TODO Zack: high level function which create a new proof object and register
+ * to it the widgets which must be refreshed upon status changes *)
+(* proof#status#attach ... *)
+ proof#status#notify ();
+ set_proof proof
+let interpreter =
+ new MatitaInterpreter.interpreter
+ ~disambiguator ~console:gui#console ~get_proof ~new_proof ()