X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=d3e39351c04804cf06a3c0fe8cfdbd21668fd6b7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e06c02297454c3e532fe877c083d9301cb6afccd;hpb=218c0062f93dd3221b0266cfbc26fd9cf787ad18;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index e06c02297..d3e39351c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -67,8 +67,6 @@ let dbd = ~database:(Helm_registry.get "db.database") () -let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; - let restore_environment_on_boot = true ;; let notify_hbugs_on_goal_change = false ;; @@ -146,7 +144,7 @@ let check_window uris = lazy (let mmlwidget = TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = let term = CicUtil.term_of_uri uri in @@ -377,14 +375,14 @@ let in (* innertypes *) let innertypesuri = UriManager.innertypesuri_of_uri uri in - Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ; + Xml.pp ~gzip:false xmlinnertypes (Some (path ^ ".types.xml")) ; Http_getter.register' innertypesuri (Helm_registry.get "local_library.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")) ; + Xml.pp ~gzip:false xml (Some (path ^ ".xml")) ; Http_getter.register' uri (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" @@ -399,7 +397,7 @@ let None -> assert false | Some bodyuri -> bodyuri in - Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ; + Xml.pp ~gzip:false bodyxml' (Some (path ^ ".body.xml")) ; Http_getter.register' bodyuri (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" @@ -450,9 +448,10 @@ let qed () = begin (*CSC: Wrong: [] is just plainly wrong *) let proof = - Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in + Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[]) + in let (acic,ids_to_inner_types,ids_to_inner_sorts) = - (rendering_window ())#output#load_proof uri proof + (rendering_window ())#output#load_proof proof in !qed_set_sensitive false ; (* let's save the theorem and register it to the getter *) @@ -460,7 +459,8 @@ let qed () = pathname_of_annuri (UriManager.buri_of_uri uri) in let list_of_universes = - CicUnivUtils.universes_of_obj uri (Cic.Constant ("",None,ty,[])) + CicUnivUtils.universes_of_obj uri + (Cic.Constant ("",None,ty,[],[])) in let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in @@ -476,7 +476,7 @@ let qed () = (* add the object to the env *) CicEnvironment.add_type_checked_term uri (( Cic.Constant ((UriManager.name_of_uri uri), - (Some bo),ty,[])),u2); + (Some bo),ty,[],[])),u2); (* FIXME: the variable list!! *) prerr_endline "-------------> FINE"; end @@ -490,10 +490,10 @@ let save_unfinished_proof () = let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in let proof_file = Helm_registry.get "gtoplevel.proof_file" in - Xml.pp ~quiet:true xml (Some proof_file_type) ; + Xml.pp ~gzip:false xml (Some proof_file_type) ; HelmLogger.log (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ; - Xml.pp ~quiet:true bodyxml (Some proof_file) ; + Xml.pp ~gzip:false bodyxml (Some proof_file) ; HelmLogger.log (`Msg (`T ("Current proof body saved to " ^ proof_file))) ;; @@ -562,15 +562,16 @@ let refresh_proof (output : TermViewer.proof_viewer) = (*CSC: Wrong: [] is just plainly wrong *) let uri = match uri with Some uri -> uri | _ -> assert false in (uri, - Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])) in - ignore (output#load_proof uri currentproof) + ignore (output#load_proof currentproof) with e -> match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> - debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))); + debug_print ("Offending proof: " ^ + CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[],[]))); raise (InvokeTactics.RefreshProofException e) let set_proof_engine_goal g = @@ -686,7 +687,7 @@ let load_unfinished_proof () = let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in let proof_file = Helm_registry.get "gtoplevel.proof_file" in match CicParser.obj_of_xml proof_file_type (Some proof_file) with - Cic.CurrentProof (_,metasenv,bo,ty,_) -> + Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> typecheck_loaded_proof metasenv bo ty ; ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)); refresh_proof output ; @@ -861,15 +862,9 @@ let let href = Gdome.domString "href" in let show_in_show_window_obj uri obj = try - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object obj - in - let mml = - ChosenTransformer.mml_of_cic_object - ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types + let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures, + ids_to_hypotheses,_,_)) = + ApplyTransformation.mml_of_cic_object obj in window#set_title (UriManager.string_of_uri uri) ; window#misc#hide () ; window#show () ; @@ -887,9 +882,9 @@ let match n with None -> () | Some n' -> - if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then + if n'#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href then let uri = - (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string + (n'#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href)#to_string in show_in_show_window_uri (UriManager.uri_of_string uri) else @@ -1378,7 +1373,7 @@ let new_inductive () = (*CSC: Da finire *) let params = [] in let tys = !get_types_and_cons () in - let obj = Cic.InductiveDefinition(tys,params,!paramsno) in + let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in let u = begin try @@ -1594,8 +1589,8 @@ let open_ () = (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*) let metasenv,bo,ty = match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with - Cic.Constant (_,Some bo,ty,_) -> [],bo,ty - | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty + Cic.Constant (_,Some bo,ty,_,_) -> [],bo,ty + | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> metasenv,bo,ty | Cic.Constant _ | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition @@ -2091,7 +2086,7 @@ let choose_selection mmlwidget (element : Gdome.element option) = let module G = Gdome in let rec aux element = if element#hasAttributeNS - ~namespaceURI:Misc.helmns + ~namespaceURI:Misc.helm_ns ~localName:(G.domString "xref") then mmlwidget#set_selection (Some element) @@ -2266,7 +2261,7 @@ class scratch_window = ~packing:(vbox#pack ~expand:true ~padding:5) () in let sequent_viewer = TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) val mutable term = Cic.Rel 1 (* dummy value *) @@ -2348,7 +2343,7 @@ object(self) ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in let _ = proofw_ref <- Some proofw in let hbox3 = @@ -2529,7 +2524,7 @@ class empty_page = ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = TermViewer.sequent_viewer - ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) method proofw = (assert false : TermViewer.sequent_viewer) @@ -2765,7 +2760,6 @@ class rendering_window output (notebook : notebook) = factory3#add_item "Reload Stylesheets" ~callback: (function _ -> - ChosenTransformer.reload_stylesheets () ; if ProofEngine.get_proof () <> None then try refresh_goals notebook ; @@ -2849,7 +2843,7 @@ end let initialize_everything () = let output = TermViewer.proof_viewer - ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object + ~mml_of_cic_object:ApplyTransformation.mml_of_cic_object ~width:350 ~height:280 () in let notebook = new notebook in