From: Claudio Sacerdoti Coen Date: Tue, 19 Nov 2002 13:53:09 +0000 (+0000) Subject: Big change: Qed saves the theorem/definition and registers it to the getter. X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=347d3c4262af67b378f4a65f735f48797ffc37a3;p=helm.git 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 eb50104af..e4af786ce 100644 --- 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 - ("

Current proof type loaded from " ^ - prooffiletype ^ "

") ; - output_html outputhtml - ("

Current proof body loaded from " ^ - prooffile ^ "

") ; - !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 + ("

Current proof type loaded from " ^ + prooffiletype ^ "

") ; + output_html outputhtml + ("

Current proof body loaded from " ^ + prooffile ^ "

") ; + !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