X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=d3e39351c04804cf06a3c0fe8cfdbd21668fd6b7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ba0615246050989f471374ef9310d0283f755311;hpb=017cd0cdd6a0bde85c25b230ffb8796d08ffc434;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index ba0615246..d3e39351c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -23,15 +23,15 @@ * http://helm.cs.unibo.it/ *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(*****************************************************************************) let debug_level = ref 1 let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s @@ -40,15 +40,12 @@ let warning s = prerr_endline ("W: " ^ s) open Printf -(* DEBUGGING *) - module MQI = MQueryInterpreter module MQIC = MQIConn module MQGT = MQGTypes module MQGU = MQGUtil module MQG = MQueryGenerator - (* first of all let's initialize the Helm_registry *) let _ = let configuration_file = "gTopLevel.conf.xml" in @@ -61,10 +58,14 @@ let _ = (* GLOBAL CONSTANTS *) -let mqi_debug_fun s = debug_print ~level:2 s -let mqi_handle = MQIC.init_if_connected ~log:mqi_debug_fun () +let mqi_handle = MQIC.init_if_connected () -let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; +let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () let restore_environment_on_boot = true ;; let notify_hbugs_on_goal_change = false ;; @@ -120,35 +121,6 @@ let argspec = in Arg.parse argspec ignore "" -(* MISC FUNCTIONS *) - -let term_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - match uri with - CTP.ConUri uri -> C.Const (uri,[]) - | CTP.VarUri uri -> C.Var (uri,[]) - | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) - | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) -;; - -let string_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - let uri' = - match uri with - CTP.ConUri uri -> UriManager.string_of_uri uri - | CTP.VarUri uri -> UriManager.string_of_uri uri - | CTP.IndTyUri (uri,tyno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) - | CTP.IndConUri (uri,tyno,consno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ - string_of_int consno - in - (* 4 = String.length "cic:" *) - String.sub uri' 4 (String.length uri' - 4) -;; - (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) (* Check window *) @@ -172,14 +144,12 @@ 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 = - term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri) - in - (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) + let term = CicUtil.term_of_uri uri in + (Cic.Cast (term, fst(CicTypeChecker.type_of_aux' [] [] term + CicUniv.empty_ugraph ))) in try mmlwidget#load_sequent [] (111,[],expr) @@ -405,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:") "" @@ -427,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:") "" @@ -465,44 +435,54 @@ let save_obj uri obj = ;; let qed () = - match ProofEngine.get_proof () with - None -> assert false - | Some (uri,[],bo,ty) -> - let uri = match uri with Some uri -> uri | _ -> assert false in - (* we want to typecheck in the ENV *) - (*let old_working = CicUniv.get_working () in - CicUniv.set_working (CicUniv.get_global ());*) - CicUniv.directly_to_env_begin () ; - prerr_endline "-------------> QED"; - if - CicReduction.are_convertible [] - (CicTypeChecker.type_of_aux' [] [] bo) ty - then - begin - (*CSC: Wrong: [] is just plainly wrong *) - let proof = 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 - in - !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; - (* add the object to the env *) - CicEnvironment.add_type_checked_term uri ( - Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[])); - (* FIXME: the variable list!! *) - (* - CicUniv.qed (); (* now the env has the right constraints *)*) - CicUniv.directly_to_env_end(); - CicUniv.reset_working (); - prerr_endline "-------------> FINE"; - end - else - raise WrongProof - | _ -> raise OpenConjecturesStillThere + match ProofEngine.get_proof () with + None -> assert false + | Some (uri,[],bo,ty) -> + let uri = match uri with Some uri -> uri | _ -> assert false in + (* we want to typecheck in the ENV *) + prerr_endline "-------------> QED"; + let ty_bo,u = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let b,u1 = CicReduction.are_convertible [] ty_bo ty u in + if b then + begin + (*CSC: Wrong: [] is just plainly wrong *) + let proof = + 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 proof + in + !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 + let list_of_universes = + 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 + (********************************************** + TASSI: to uncomment whe universes will be ON + ***********************************************) + (* + make_dirs pathname ; + save_object_to_disk uri acic ids_to_inner_sorts + ids_to_inner_types pathname; + *) + (* save the universe graph u2 *) + (* add the object to the env *) + CicEnvironment.add_type_checked_term uri (( + Cic.Constant ((UriManager.name_of_uri uri), + (Some bo),ty,[],[])),u2); + (* FIXME: the variable list!! *) + prerr_endline "-------------> FINE"; + end + else + raise WrongProof + | _ -> raise OpenConjecturesStillThere ;; (** save an unfinished proof on the filesystem *) @@ -510,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))) ;; @@ -524,11 +504,11 @@ let typecheck_loaded_proof metasenv bo ty = ignore ( List.fold_left (fun metasenv ((_,context,ty) as conj) -> - ignore (T.type_of_aux' metasenv context ty) ; + ignore (T.type_of_aux' metasenv context ty CicUniv.empty_ugraph) ; metasenv @ [conj] ) [] metasenv) ; - ignore (T.type_of_aux' metasenv [] ty) ; - ignore (T.type_of_aux' metasenv [] bo) + ignore (T.type_of_aux' metasenv [] ty CicUniv.empty_ugraph) ; + ignore (T.type_of_aux' metasenv [] bo CicUniv.empty_ugraph) ;; let decompose_uris_choice_callback uris = @@ -536,9 +516,9 @@ let decompose_uris_choice_callback uris = let module U = UriManager in List.map (function uri -> - match MQueryMisc.cic_textual_parser_uri_of_string uri with - CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) - | _ -> assert false) + match CicUtil.term_of_uri uri with + | Cic.MutInd (uri, typeno, _) -> (uri, typeno, []) + | _ -> assert false) (interactive_user_uri_choice ~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" @@ -551,7 +531,7 @@ let decompose_uris_choice_callback uris = let mk_fresh_name_callback metasenv context name ~typ = let fresh_name = - match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with + match FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ with Cic.Name fresh_name -> fresh_name | Cic.Anonymous -> assert false in @@ -582,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 = @@ -636,7 +617,7 @@ let refresh_goals ?(empty_notebook=true) notebook = begin notebook#set_current_page ~may_skip_switch_page_event:true metano ; - notebook#proofw#load_sequent metasenv currentsequent + notebook#proofw#load_sequent metasenv currentsequent ; end with e -> @@ -676,6 +657,7 @@ module InvokeTacticsCallbacks = let decompose_uris_choice_callback = decompose_uris_choice_callback let mk_fresh_name_callback = mk_fresh_name_callback let mqi_handle = mqi_handle + let dbd = dbd end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -705,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 ; @@ -880,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 () ; @@ -899,16 +875,16 @@ let (`Error (`T (Printexc.to_string e))) in let show_in_show_window_uri uri = - let obj = CicEnvironment.get_obj uri in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in show_in_show_window_obj uri obj in let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) = 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 @@ -939,21 +915,12 @@ let user_uri_choice ~title ~msg uris = ;; let locate_callback id = - let query = MQG.locate id in - let result = MQI.execute mqi_handle query in - let uris = - List.map - (function uri,_ -> - MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri) - result in - HelmLogger.log (`Msg (`T "Locate Query:")) ; - MQueryUtil.text_of_query (fun m -> HelmLogger.log (`Msg (`T m))) "" query; + let uris = MetadataQuery.locate ~dbd id in + HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ; HelmLogger.log (`Msg (`T "Result:")) ; - MQueryUtil.text_of_result (fun m -> HelmLogger.log (`Msg (`T m))) "" result; + List.iter (fun uri -> HelmLogger.log (`Msg (`T uri))) uris; user_uri_choice ~title:"Ambiguous input." - ~msg: - ("Ambiguous input \"" ^ id ^ - "\". Please, choose one interpetation:") + ~msg:(sprintf "Ambiguous input \"%s\". Please, choose one interpetation:" id) uris ;; @@ -1007,7 +974,7 @@ let input_or_locate_uri ~title = HelmLogger.log (`Msg (`T "OK")) ; true with - Http_getter_types.Unresolvable_URI _ -> + Http_getter_types.Key_not_found _ -> HelmLogger.log (`Error (`T ("URI " ^ uri ^ " does not correspond to any object."))) ; @@ -1190,7 +1157,7 @@ let new_inductive () = try ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with Http_getter_types.Unresolvable_URI _ -> + with Http_getter_types.Key_not_found _ -> get_uri := (function () -> uri) ; get_names := (function () -> names) ; inductive := inductiveb#active ; @@ -1220,7 +1187,7 @@ let new_inductive () = ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TermEditor'.term_editor - mqi_handle + ~dbd ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () ~isnotempty_callback: @@ -1261,7 +1228,7 @@ let new_inductive () = (fun name (newinputt,cons_names_entry) -> let consnamesstr = cons_names_entry#text in let cons_names = Str.split (Str.regexp " +") consnamesstr in - let metasenv,expr = + let metasenv,expr,ugraph = newinputt#get_metasenv_and_term ~context:[] ~metasenv:[] in match metasenv with @@ -1332,7 +1299,7 @@ let new_inductive () = ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TermEditor'.term_editor - mqi_handle + ~dbd ~width:400 ~height:20 ~packing:scrolled_window#add ~share_environment_with:inputt () ~isnotempty_callback: @@ -1363,7 +1330,7 @@ let new_inductive () = let cons_types = List.map2 (fun name inputt -> - let metasenv,expr = + let metasenv,expr,ugraph = inputt#get_metasenv_and_term ~context ~metasenv:[] in match metasenv with @@ -1406,23 +1373,30 @@ let new_inductive () = (*CSC: Da finire *) let params = [] in let tys = !get_types_and_cons () in - let obj = Cic.InductiveDefinition(tys,params,!paramsno) in - begin - try - debug_print (CicPp.ppobj obj); - CicTypeChecker.typecheck_mutual_inductive_defs uri - (tys,params,!paramsno) ; - with - e -> - debug_print "Offending mutual (co)inductive type declaration:" ; - debug_print (CicPp.ppobj obj) ; - end ; + let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in + let u = + begin + try + debug_print (CicPp.ppobj obj); + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,!paramsno) CicUniv.empty_ugraph + with + e -> + debug_print "Offending mutual (co)inductive type declaration:" ; + debug_print (CicPp.ppobj obj) ; + (* I think we should fail here! *) + CicUniv.empty_ugraph + end + in (* We already know that obj is well-typed. We need to add it to the *) (* environment in order to compute the inner-types without having to *) (* debrujin it or having to modify lots of other functions to avoid *) (* asking the environment for the MUTINDs we are defining now. *) - CicEnvironment.put_inductive_definition uri obj ; + + (* u should be cleaned before adding it to the env *) + CicEnvironment.put_inductive_definition uri (obj,u) ; save_obj uri obj ; + (* TASSI: FIXME we should save the cleaned u here *) show_in_show_window_obj uri obj with e -> @@ -1478,7 +1452,7 @@ let new_proof () = (* moved here to have visibility of the ok button *) let newinputt = TermEditor'.term_editor - mqi_handle + ~dbd ~width:400 ~height:100 ~packing:scrolled_window#add ~share_environment_with:inputt () ~isnotempty_callback: @@ -1501,7 +1475,7 @@ let new_proof () = (function () -> chosen := true ; try - let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in + let metasenv,parsed,ugraph = newinputt#get_metasenv_and_term [] [] in let uristr = "cic:" ^ uri_entry#text in let uri = UriManager.uri_of_string uristr in if String.sub uristr (String.length uristr - 4) 4 <> ".con" then @@ -1511,7 +1485,7 @@ let new_proof () = try ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with Http_getter_types.Unresolvable_URI _ -> + with Http_getter_types.Key_not_found _ -> get_metasenv_and_term := (function () -> metasenv,parsed) ; get_uri := (function () -> uri) ; window#destroy () @@ -1553,7 +1527,9 @@ let new_proof () = let check_term_in_scratch scratch_window metasenv context expr = try - let ty = CicTypeChecker.type_of_aux' metasenv context expr in + let ty,ugraph = + CicTypeChecker.type_of_aux' metasenv context expr CicUniv.empty_ugraph + in let expr = Cic.Cast (expr,ty) in scratch_window#show () ; scratch_window#set_term expr ; @@ -1583,8 +1559,10 @@ let check scratch_window () = canonical_context in try - let metasenv',expr = inputt#get_metasenv_and_term context metasenv in - check_term_in_scratch scratch_window metasenv' context expr + let metasenv',expr,ugraph = + inputt#get_metasenv_and_term context metasenv + in + check_term_in_scratch scratch_window metasenv' context expr with e -> HelmLogger.log @@ -1607,12 +1585,12 @@ let open_ () = let notebook = (rendering_window ())#notebook in try let uri = input_or_locate_uri ~title:"Open" in - ignore(CicTypeChecker.typecheck uri); + ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph); (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*) let metasenv,bo,ty = - match CicEnvironment.get_cooked_obj uri with - Cic.Constant (_,Some bo,ty,_) -> [],bo,ty - | Cic.CurrentProof (_,metasenv,bo,ty,_) -> 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 _ | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition @@ -1665,16 +1643,13 @@ let show_query_results results = (clist#connect#select_row (fun ~row ~column ~event -> let (uristr,_) = List.nth results row in - match - MQueryMisc.cic_textual_parser_uri_of_string - (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' - uristr) - with - CicTextualParser0.ConUri uri - | CicTextualParser0.VarUri uri - | CicTextualParser0.IndTyUri (uri,_) - | CicTextualParser0.IndConUri (uri,_,_) -> + match CicUtil.term_of_uri uristr with + | Cic.Const (uri, _) + | Cic.Var (uri, _) + | Cic.MutInd (uri, _, _) + | Cic.MutConstruct (uri, _, _, _) -> show_in_show_window_uri uri + | _ -> assert false ) ) ; window#show () @@ -1875,7 +1850,8 @@ let refine_constraints (must_obj,must_rel,must_sort) = let completeSearchPattern () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in try - let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in + let metasenv,expr,ugraph = + inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in let must = CGSearchPattern.get_constraints expr in let must',only = refine_constraints must in let query = @@ -2092,10 +2068,7 @@ let searchPattern () = match !ProofEngine.goal with | None -> () | Some metano -> - let uris' = - TacticChaser.matchConclusion mqi_handle - ~choose_must () (proof, metano) - in + let uris' = List.map fst (MetadataQuery.hint ~dbd (proof, metano)) in let uri' = user_uri_choice ~title:"Ambiguous input." ~msg: "Many lemmas can be successfully applied. Please, choose one:" @@ -2113,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) @@ -2288,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 *) @@ -2370,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 = @@ -2551,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) @@ -2787,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 ; @@ -2824,7 +2796,7 @@ class rendering_window output (notebook : notebook) = ~packing:frame#add () in let inputt = TermEditor'.term_editor - mqi_handle + ~dbd ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: (function b -> @@ -2871,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 @@ -2900,6 +2872,7 @@ let main () = ;; try +(* CicEnvironment.set_trust (fun _ -> false); *) Sys.catch_break true; main (); with Sys.Break -> () (* exit nicely, invoking at_exit functions *)