open MatitaTypes
open MatitaMisc
-(** {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 dbd =
Mysql.quick_connect
~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")
()
+let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner")
let gui = MatitaGui.instance ()
let disambiguator =
new MatitaDisambiguator.disambiguator ~parserr ~dbd
~chooseUris:(interactive_user_uri_choice ~gui)
~chooseInterp:(interactive_interp_choice ~gui)
()
+
+let currentProof = new MatitaProof.currentProof
+
let proof_viewer = MatitaMathView.proof_viewer_instance ()
let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
let sequents_viewer =
let set_goal goal =
- if not (has_proof ()) then assert false;
- (get_proof ())#set_goal goal
+ if not (currentProof#onGoing ()) then assert false;
+ currentProof#proof#set_goal goal
in
MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
~sequent_viewer ~set_goal ()
-
-let new_proof (proof: MatitaTypes.proof) =
+let _ = (* attach observers to proof status *)
let proof_observer _ (status, ()) =
let ((uri_opt, _, _, _), _) = status in
proof_viewer#load_proof status;
sequents_viewer#load_sequents metasenv;
sequents_viewer#goto_sequent goal)
in
- ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- sequents_observer);
- ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
- proof_observer);
- proof#notify;
- set_proof (Some proof)
-
-let quit () = (* quit program, asking for confirmation if needed *)
- if not (has_proof ()) ||
- (ask_confirmation ~gui
- ~msg:("Proof in progress, are you sure you want to quit?") ())
- then
- GMain.Main.quit ()
-
-let abort_proof () =
- if has_proof () then begin
- set_proof None;
- sequents_viewer#reset
- end
-
-let proof_handler =
- { MatitaTypes.get_proof = get_proof;
- MatitaTypes.abort_proof = abort_proof;
- MatitaTypes.set_proof = set_proof;
- MatitaTypes.has_proof = has_proof;
- MatitaTypes.new_proof = new_proof;
- MatitaTypes.quit = quit;
- }
-
+ currentProof#addObserver sequents_observer;
+ currentProof#addObserver proof_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 mathViewer = MatitaMathView.mathViewer ()
let interpreter =
- let console = gui#console in
- new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console ()
+ let console = (gui#console :> MatitaTypes.console) in
+ let currentProof = (currentProof :> MatitaTypes.currentProof) in
+ new MatitaInterpreter.interpreter
+ ~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 script_forward _ =
let buf = gui#script#scriptTextView#buffer in
let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
- if
+ let (success, hide) =
interpreter#evalPhrase
- (buf#get_text ~start:locked_iter ~stop:buf#end_iter ());
- then
+ (buf#get_text ~start:locked_iter ~stop:buf#end_iter ())
+ in
+ if success then
gui#lockScript (locked_iter#offset + interpreter#endOffset)
let script_jump _ =
let len = String.length raw_text in
let rec parse offset =
if offset < len then begin
- if
- interpreter#evalPhrase ~transparent:true
- (String.sub raw_text offset (len - offset));
- then begin
+ let (success, hide) =
+ interpreter#evalPhrase (String.sub raw_text offset (len - offset))
+ in
+ if success then begin
let new_offset = interpreter#endOffset + offset in
gui#lockScript (new_offset + locked_iter#offset);
parse new_offset
(** {2 GUI callbacks} *)
let _ =
- gui#setQuitCallback quit;
+ gui#setQuitCallback currentProof#quit;
gui#setPhraseCallback interpreter#evalPhrase;
gui#main#debugMenu#misc#hide ();
- ignore (gui#main#newProofMenuItem#connect#activate
- (gui#console#show ~msg:"theorem "));
+ ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
+ gui#console#clear ();
+ gui#console#show ~msg:"theorem " ()));
ignore (gui#main#openMenuItem#connect#activate (fun _ ->
match gui#chooseFile () with
| None -> ()
Helm_registry.set_bool "matita.auto_disambiguation"
(not (Helm_registry.get_bool "matita.auto_disambiguation")));
addDebugItem "dump proof status to stdout" (fun _ ->
- print_endline ((get_proof ())#toString));
- addDebugItem "hide console" gui#console#hide;
- addDebugItem "show console" gui#console#show;
+ print_endline (currentProof#proof#toString));
+ addDebugItem "dump environment to \"env.dump\"" (fun _ ->
+ let oc = open_out "env.dump" in
+ CicEnvironment.dump_to_channel oc;
+ close_out oc);
+ addDebugItem "print selected terms" (fun () ->
+ 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)
end
(** </DEBUGGING> *)
let _ =
+(* CicEnvironment.set_trust (fun _ -> false); *)
(try
load_script Sys.argv.(1)
with Invalid_argument _ -> ());
+ gui#console#show ();
GtkThread.main ()
projects / helm.git / blobdiff