ProofEngine.proof is now an abstract data type (since we plan to have OMDoc

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 7c28c22ced477ee65adad54bba34af1d2c5ed763..7ed63cb102abdbc20c0072b4812254cda01a4488 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -480,7 +480,7 @@ let save_obj uri obj =
 ;;
 
 let qed () =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
     None -> assert false
   | Some (uri,[],bo,ty) ->
      if
@@ -569,10 +569,10 @@ let mk_fresh_name_callback context name ~typ =
 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 ;
@@ -587,7 +587,7 @@ let refresh_proof (output : TermViewer.proof_viewer) =
    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 ;
@@ -606,7 +606,7 @@ let refresh_goals ?(empty_notebook=true) notebook =
        notebook#proofw#unload
    | Some metano ->
       let metasenv =
-       match !ProofEngine.proof with
+       match ProofEngine.get_proof () with
           None -> assert false
         | Some (_,metasenv,_,_) -> metasenv
       in
@@ -642,7 +642,7 @@ let metano =
    | Some m -> m
 in
 let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
     None -> assert false
   | Some (_,metasenv,_,_) -> metasenv
 in
@@ -701,8 +701,8 @@ let load_unfinished_proof () =
         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.set_proof
+             (Some (uri, metasenv, bo, ty)) ;
             ProofEngine.goal :=
              (match metasenv with
                  [] -> None
@@ -876,7 +876,7 @@ let setgoal metano =
  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
@@ -1579,8 +1579,8 @@ prerr_endline ("######################## " ^ xxx) ;
   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.set_proof
+      (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
      ProofEngine.goal := Some 1 ;
      refresh_goals notebook ;
      refresh_proof output ;
@@ -1622,7 +1622,7 @@ let check scratch_window () =
  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
@@ -1671,8 +1671,8 @@ let open_ () =
        | Cic.Variable _
        | Cic.InductiveDefinition _ -> raise NotADefinition
      in
-      ProofEngine.proof :=
-       Some (uri, metasenv, bo, ty) ;
+      ProofEngine.set_proof
+       (Some (uri, metasenv, bo, ty)) ;
       ProofEngine.goal := None ;
       refresh_goals notebook ;
       refresh_proof output ;
@@ -2143,7 +2143,7 @@ let searchPattern () =
  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
@@ -2830,7 +2830,7 @@ class rendering_window output (notebook : notebook) =
    ~callback:
      (function _ ->
        ApplyStylesheets.reload_stylesheets () ;
-       if !ProofEngine.proof <> None then
+       if ProofEngine.get_proof () <> None then
         try
          refresh_goals notebook ;
          refresh_proof output