X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=8ec91964edff51159a58bb197e2d57f5bdc31aa2;hb=5379335718a93d3e933d9bfdc0dd85f00983bc21;hp=eb50104af4f5a554e6c63aae5885d5e58c7ecb70;hpb=a9e833b37216b225262450fd4e3fa5bf79ae4c3a;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index eb50104af..8ec91964e 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -530,11 +530,12 @@ let
 =
 (*CSC: ????????????????? *)
  let xml, bodyxml =
-  Cic2Xml.print_object uri ~ids_to_inner_sorts annobj 
+  Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
+   annobj 
  in
  let xmlinnertypes =
-  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
-   ~ids_to_inner_types
+  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+   ~ask_dtd_to_the_getter:true
  in
   let input =
    match bodyxml with
@@ -551,6 +552,55 @@ 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 ~ask_dtd_to_the_getter:false
+    annobj 
+  in
+  let xmlinnertypes =
+   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+    ~ask_dtd_to_the_getter:false
+  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 +741,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 +772,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,
@@ -723,12 +788,6 @@ let qed () =
   | _ -> raise OpenConjecturesStillThere
 ;;
 
-(*????
-let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
-let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
-*)
-let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
-
 let save () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   match !ProofEngine.proof with
@@ -742,7 +801,10 @@ let save () =
         Cic2acic.acic_object_of_cic_object currentproof
        in
         let xml, bodyxml =
-         match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
+         match
+          Cic2Xml.print_object uri ~ids_to_inner_sorts
+           ~ask_dtd_to_the_getter:true acurrentproof
+         with
             xml,Some bodyxml -> xml,bodyxml
           | _,None -> assert false
         in
@@ -774,27 +836,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 +1401,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 +2479,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 +2490,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