;;
let qed () =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,[],bo,ty) ->
if
let refresh_proof (output : TermViewer.proof_viewer) =
try
let uri,currentproof =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- ProofEngine.proof := Some(uri,metasenv,bo,ty);
+ ProofEngine.set_proof (Some (uri,metasenv,bo,ty)) ;
if List.length metasenv = 0 then
begin
!qed_set_sensitive true ;
ignore (output#load_proof uri currentproof)
with
e ->
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (InvokeTactics.RefreshProofException e)
+let set_proof_engine_goal g =
+ ProofEngine.goal := g
+;;
+
let refresh_goals ?(empty_notebook=true) notebook =
try
match !ProofEngine.goal with
notebook#proofw#unload
| Some metano ->
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
notebook#remove_all_pages ~skip_switch_page_event ;
List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
in
- if empty_notebook then
- begin
- regenerate_notebook () ;
- notebook#set_current_page
- ~may_skip_switch_page_event:false metano
- end
- else
- begin
- notebook#set_current_page
- ~may_skip_switch_page_event:true metano ;
- notebook#proofw#load_sequent metasenv currentsequent
- end
+ if empty_notebook then
+ begin
+ regenerate_notebook () ;
+ notebook#set_current_page
+ ~may_skip_switch_page_event:false metano
+ end
+ else
+ begin
+ notebook#set_current_page
+ ~may_skip_switch_page_event:true metano ;
+ notebook#proofw#load_sequent metasenv currentsequent
+ end
with
e ->
let metano =
| Some m -> m
in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
match CicParser.obj_of_xml prooffiletype (Some prooffile) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
- ProofEngine.proof :=
- Some (uri, metasenv, bo, ty) ;
- ProofEngine.goal :=
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ refresh_proof output ;
+ set_proof_engine_goal
(match metasenv with
[] -> None
| (metano,_,_)::_ -> Some metano
) ;
- refresh_proof output ;
refresh_goals notebook ;
output_html outputhtml
("<h1 color=\"Green\">Current proof type loaded from " ^
let notebook = (rendering_window ())#notebook in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
try
let metasenv,expr = !get_metasenv_and_term () in
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
- ProofEngine.proof :=
- Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
- ProofEngine.goal := Some 1 ;
+ ProofEngine.set_proof
+ (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
+ set_proof_engine_goal (Some 1) ;
refresh_goals notebook ;
refresh_proof output ;
!save_set_sensitive true ;
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> []
| Some (_,metasenv,_,_) -> metasenv
in
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
in
- ProofEngine.proof :=
- Some (uri, metasenv, bo, ty) ;
- ProofEngine.goal := None ;
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ set_proof_engine_goal None ;
refresh_goals notebook ;
refresh_proof output ;
!save_set_sensitive true
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let proof =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some proof -> proof
in
if not skip then
try
let (metano,setgoal,page) = List.nth !pages i in
- ProofEngine.goal := Some metano ;
+ set_proof_engine_goal (Some metano) ;
Lazy.force (page#compute) ;
Lazy.force setgoal;
if notify_hbugs_on_goal_change then
~callback:
(function _ ->
ApplyStylesheets.reload_stylesheets () ;
- if !ProofEngine.proof <> None then
+ if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
refresh_proof output