Big change: Qed saves the theorem/definition and registers it to the getter.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index eb50104af4f5a554e6c63aae5885d5e58c7ecb70..e4af786ceb2e4e81a83f6f2c109f4bb881cf6ec4 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -551,6 +551,54 @@ let
     output
 ;;
 
+let
+ save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
+=
+ let name =
+  let struri = UriManager.string_of_uri uri in
+  let idx = (String.rindex struri '/') + 1 in
+   String.sub struri idx (String.length struri - idx)
+ in
+  let path = pathname ^ "/" ^ name in
+  let xml, bodyxml =
+   Cic2Xml.print_object uri ~ids_to_inner_sorts annobj 
+  in
+  let xmlinnertypes =
+   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
+    ~ids_to_inner_types
+  in
+   (* innertypes *)
+   let innertypesuri = UriManager.innertypesuri_of_uri uri in
+    Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
+    Getter.register innertypesuri
+     (Configuration.annotations_url ^
+       Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri innertypesuri) ^ ".xml"
+     ) ;
+    (* constant type / variable / mutual inductive types definition *)
+    Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
+    Getter.register uri
+     (Configuration.annotations_url ^
+       Str.replace_first (Str.regexp "^cic:") ""
+        (UriManager.string_of_uri uri) ^ ".xml"
+     ) ;
+    match bodyxml with
+       None -> ()
+     | Some bodyxml' ->
+        (* constant body *)
+        let bodyuri =
+         match UriManager.bodyuri_of_uri uri with
+            None -> assert false
+          | Some bodyuri -> bodyuri
+        in
+         Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
+         Getter.register bodyuri
+          (Configuration.annotations_url ^
+            Str.replace_first (Str.regexp "^cic:") ""
+             (UriManager.string_of_uri bodyuri) ^ ".xml"
+          )
+;;
+
 
 (* CALLBACKS *)
 
@@ -691,6 +739,15 @@ let mml_of_cic_term metano term =
 exception OpenConjecturesStillThere;;
 exception WrongProof;;
 
+let pathname_of_annuri uristring =
+ Configuration.annotations_dir ^    
+  Str.replace_first (Str.regexp "^cic:") "" uristring
+;;
+
+let make_dirs dirpath =
+ ignore (Unix.system ("mkdir -p " ^ dirpath))
+;;
+
 let qed () =
  match !ProofEngine.proof with
     None -> assert false
@@ -713,6 +770,12 @@ let qed () =
            ids_to_inner_types
          in
           ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
+          !qed_set_sensitive false ;
+          (* let's save the theorem and register it to the getter *) 
+          let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
+          make_dirs pathname ;
+          save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
+           pathname ;
           current_cic_infos :=
            Some
             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
@@ -774,27 +837,33 @@ let load () =
  let output = ((rendering_window ())#output : GMathView.math_view) in
  let notebook = (rendering_window ())#notebook in
   try
-   let uri = UriManager.uri_of_string "cic:/dummy.con" 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 :=
-         (match metasenv with
-             [] -> None
-           | (metano,_,_)::_ -> Some metano
-         ) ;
-        refresh_proof output ;
-        refresh_sequent notebook ;
-         output_html outputhtml
-          ("<h1 color=\"Green\">Current proof type loaded from " ^
-            prooffiletype ^ "</h1>") ;
-         output_html outputhtml
-          ("<h1 color=\"Green\">Current proof body loaded from " ^
-            prooffile ^ "</h1>") ;
-        !save_set_sensitive true
-     | _ -> assert false
+   match 
+    GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
+     "Choose an URI:"
+   with
+      None -> raise NoChoice
+    | Some uri0 ->
+       let uri = UriManager.uri_of_string ("cic:" ^ uri0) 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 :=
+             (match metasenv with
+                 [] -> None
+               | (metano,_,_)::_ -> Some metano
+             ) ;
+            refresh_proof output ;
+            refresh_sequent notebook ;
+             output_html outputhtml
+              ("<h1 color=\"Green\">Current proof type loaded from " ^
+                prooffiletype ^ "</h1>") ;
+             output_html outputhtml
+              ("<h1 color=\"Green\">Current proof body loaded from " ^
+                prooffile ^ "</h1>") ;
+            !save_set_sensitive true
+         | _ -> assert false
   with
      RefreshSequentException e ->
       output_html outputhtml
@@ -1333,7 +1402,7 @@ let new_proof () =
  let non_empty_type = ref false in
  let window =
   GWindow.window
-   ~width:600 ~modal:true ~title:"New Proof or Definition..."
+   ~width:600 ~modal:true ~title:"New Proof or Definition"
    ~border_width:2 () in
  let vbox = GPack.vbox ~packing:window#add () in
  let hbox =
@@ -2411,7 +2480,7 @@ class rendering_window output (notebook : notebook) =
  let export_to_postscript_menu_item =
   begin
    let _ =
-    factory1#add_item "New Proof or Definition" ~key:GdkKeysyms._N
+    factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
      ~callback:new_proof
    in
    let reopen_menu_item =
@@ -2422,7 +2491,7 @@ class rendering_window output (notebook : notebook) =
     factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
    ignore (factory1#add_separator ()) ;
    ignore
-    (factory1#add_item "Load Unfinished Proof" ~key:GdkKeysyms._L
+    (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
       ~callback:load) ;
    let save_menu_item =
     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save