=
(*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
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 *)
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
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,
| _ -> 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
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
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
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 =
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 =
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
projects / helm.git / blobdiff