From 36f71caeee72cb15185ecbc7644ed1da5c6f8186 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 13 May 2004 12:59:43 +0000
Subject: [PATCH] changed proofStatus so that uri component is optional (useful
 to start an unnamed proof or leave the possibility of postpone uri choice)

---
 helm/gTopLevel/gTopLevel.ml            | 12 +++++++-----
 helm/gTopLevel/proofEngine.ml          |  1 +
 helm/ocaml/tactics/proofEngineTypes.ml |  2 +-
 3 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e70946564..1726725c1 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -468,6 +468,7 @@ let qed () =
  match ProofEngine.get_proof () with
     None -> assert false
   | Some (uri,[],bo,ty) ->
+     let uri = match uri with Some uri -> uri | _ -> assert false in
      if
       CicReduction.are_convertible []
        (CicTypeChecker.type_of_aux' [] [] bo) ty
@@ -565,8 +566,9 @@ let refresh_proof (output : TermViewer.proof_viewer) =
        else
         Hbugs.notify () ;
        (*CSC: Wrong: [] is just plainly wrong *)
-       uri,
-        (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
+        let uri = match uri with Some uri -> uri | _ -> assert false in
+        (uri,
+         Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
   in
    ignore (output#load_proof uri currentproof)
  with
@@ -691,7 +693,7 @@ let load_unfinished_proof () =
         match CicParser.obj_of_xml proof_file_type (Some proof_file) with
            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
             typecheck_loaded_proof metasenv bo ty ;
-            ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+            ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty));
             refresh_proof output ;
             set_proof_engine_goal
              (match metasenv with
@@ -1512,7 +1514,7 @@ let new_proof () =
    let metasenv,expr = !get_metasenv_and_term () in
     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
      ProofEngine.set_proof
-      (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
+      (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr));
      set_proof_engine_goal (Some 1) ;
      refresh_goals notebook ;
      refresh_proof output ;
@@ -1600,7 +1602,7 @@ let open_ () =
        | Cic.Variable _
        | Cic.InductiveDefinition _ -> raise NotADefinition
      in
-      ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+      ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ;
       set_proof_engine_goal None ;
       refresh_goals notebook ;
       refresh_proof output ;
diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 20863f1a9..d9b6219b2 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -38,6 +38,7 @@ let get_current_status_as_xml () =
   match get_proof () with
      None -> assert false
    | Some (uri, metasenv, bo, ty) ->
+      let uri = match uri with Some uri -> uri | None -> assert false in
       let currentproof =
        (*CSC: Wrong: [] is just plainly wrong *)
        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml
index d668090e4..3e0a12e4e 100644
--- a/helm/ocaml/tactics/proofEngineTypes.ml
+++ b/helm/ocaml/tactics/proofEngineTypes.ml
@@ -26,7 +26,7 @@
   (**
     current proof (proof uri * metas * (in)complete proof * term to be prooved)
   *)
-type proof = UriManager.uri * Cic.metasenv * Cic.term * Cic.term
+type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term
   (** current goal, integer index *)
 type goal = int
 type status = proof * goal
-- 
2.39.2