-exception Not_implemented of string
-let not_implemented feature = raise (Not_implemented feature)
-
- (** exceptions whose content should be presented to the user *)
-exception Failure of string
-let error s = raise (Failure s)
-
-let _ = Helm_registry.load_from "matita.conf.xml"
-let _ = GMain.Main.init ()
-let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
-
-let interactive_user_uri_choice
- ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=false) ~title ~msg
- uris
-=
- let only_constant_choices =
- lazy
- (List.filter
- (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
- uris)
+open Printf
+
+open MatitaGtkMisc
+open MatitaTypes
+open MatitaMisc
+
+module DB = BuildTimeConf.DB
+
+(** {2 Internal status} *)
+
+let (get_proof, set_proof, has_proof) =
+ let (current_proof: MatitaTypes.proof option ref) = ref None in
+ ((fun () -> (* get_proof *)
+ match !current_proof with
+ | Some proof -> proof
+ | None -> failwith "No current proof"),
+ (fun proof -> (* set_proof *)
+ current_proof := proof),
+ (fun () -> (* has_proof *)
+ !current_proof <> None))
+
+(** {2 Initialization} *)
+
+let _ =
+ Helm_registry.load_from "matita.conf.xml";
+ GtkMain.Rc.add_default_file BuildTimeConf.gtkrc;
+ GMain.Main.init ()
+let parserr = new MatitaDisambiguator.parserr ()
+let dbh =
+ new DB.connection ~host:(Helm_registry.get "db.host")
+ ~user:(Helm_registry.get "db.user") (Helm_registry.get "db.database")
+let gui = MatitaGui.instance ()
+let disambiguator =
+ new MatitaDisambiguator.disambiguator ~parserr ~dbh
+ ~chooseUris:(interactive_user_uri_choice ~gui)
+ ~chooseInterp:(interactive_interp_choice ~gui)
+ ()
+let proof_viewer =
+ let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in
+ MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) ()
+let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
+let sequents_viewer =
+ let set_goal goal =
+ debug_print (sprintf "Setting goal %d" goal);
+ if not (has_proof ()) then assert false;
+ (get_proof ())#set_goal goal