From 9a7c77e5c29d764109a104aa629761ba90cb511c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Jun 2009 08:40:48 +0000 Subject: [PATCH] Useless GrafiteTypes.get_baseuri removed. --- helm/software/components/grafite_engine/grafiteEngine.ml | 8 ++++---- helm/software/components/grafite_engine/grafiteTypes.ml | 2 -- helm/software/components/grafite_engine/grafiteTypes.mli | 2 -- helm/software/matita/matita.ml | 2 +- helm/software/matita/matitaEngine.ml | 4 ++-- helm/software/matita/matitaGui.ml | 4 ++-- helm/software/matita/matitaWiki.ml | 9 ++++----- 7 files changed, 13 insertions(+), 18 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index b1cc9d671..192e396af 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -520,7 +520,7 @@ let eval_coercion status ~add_composites uri arity saturations = let status, lemmas = GrafiteSync.add_coercion ~add_composites ~pack_coercion_obj:CicRefine.pack_coercion_obj - status uri arity saturations (GrafiteTypes.get_baseuri status) in + status uri arity saturations status#baseuri in let moo_content = coercion_moo_statement_of (uri,arity,saturations,0) in let status = GrafiteTypes.add_moo_content [moo_content] status in add_coercions_of_lemmas lemmas status @@ -724,7 +724,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = in let estatus,obj = GrafiteDisambiguate.disambiguate_nobj estatus - ~baseuri:(GrafiteTypes.get_baseuri status) (text,prefix_len,obj) in + ~baseuri:status#baseuri (text,prefix_len,obj) in let uri,height,nmenv,nsubst,nobj = obj in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in let status = @@ -792,7 +792,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status in res,`Old uris | GrafiteAst.Inverter (loc, name, indty, params) -> - let buri = GrafiteTypes.get_baseuri status in + let buri = status#baseuri in let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in let indty_uri = try CicUtil.uri_of_term indty @@ -881,7 +881,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status ".ind", (match types with (name,_,_,_)::_ -> name | _ -> assert false) | _ -> assert false in - let buri = GrafiteTypes.get_baseuri status in + let buri = status#baseuri in let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ext) in let obj = CicRefine.pack_coercion_obj obj in let metasenv = GrafiteTypes.get_proof_metasenv status in diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 9fd40b1c4..959d96f36 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -166,8 +166,6 @@ let add_moo_content cmds status = GrafiteAstPp.pp_command content')); *) status#set_moo_content_rev content' -let get_baseuri status = status#baseuri;; - let dump_status status = HLog.message "status.aliases:\n"; HLog.message "status.proof_status:"; diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index c30beead0..34e3d0966 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -76,8 +76,6 @@ val dump_status : status -> unit (** list is not reversed, head command will be the first emitted *) val add_moo_content: GrafiteMarshal.ast_command list -> status -> status -val get_baseuri: status -> string - val get_current_proof: status -> ProofEngineTypes.proof val get_proof_metasenv: status -> Cic.metasenv val get_stack: status -> Continuationals.Stack.t diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index e9965c4ca..1b4cc5a3c 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -333,7 +333,7 @@ let _ = prerr_endline "Still cleaning the library: don't be impatient!")); prerr_endline "Matita is cleaning up. Please wait."; let baseuri = - GrafiteTypes.get_baseuri (MatitaScript.current ())#grafite_status + (MatitaScript.current ())#grafite_status#baseuri in LibraryClean.clean_baseuris [baseuri] diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index 6b16891c8..ba4e34696 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -41,7 +41,7 @@ let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal t GrafiteTypes.set_metasenv metasenv grafite_status,tac let disambiguate_command lexicon_status_ref grafite_status cmd = - let baseuri = GrafiteTypes.get_baseuri grafite_status in + let baseuri = grafite_status#baseuri in let lexicon_status,metasenv,cmd = GrafiteDisambiguate.disambiguate_command ~baseuri !lexicon_status_ref (GrafiteTypes.get_proof_metasenv grafite_status) cmd @@ -62,7 +62,7 @@ let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) = let lexicon_status = GrafiteTypes.get_estatus grafite_status in let dump = not (Helm_registry.get_bool "matita.moo") in let lexicon_status_ref = ref (lexicon_status :> LexiconEngine.status) in - let baseuri = GrafiteTypes.get_baseuri grafite_status in + let baseuri = grafite_status#baseuri in let new_grafite_status,new_objs = match ast with | G.Executable (_, G.Command (_, G.Coercion _)) when dump -> diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 7b5a929cb..5272f07a7 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -67,11 +67,11 @@ class console ~(buffer: GText.buffer) () = end let clean_current_baseuri grafite_status = - LibraryClean.clean_baseuris [GrafiteTypes.get_baseuri grafite_status] + LibraryClean.clean_baseuris [grafite_status#baseuri] let save_moo grafite_status = let script = MatitaScript.current () in - let baseuri = GrafiteTypes.get_baseuri grafite_status in + let baseuri = grafite_status#baseuri in let no_pstatus = grafite_status#proof_status = GrafiteTypes.No_proof in diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index b52e75741..30c7fc9ea 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -64,7 +64,7 @@ let clean_exit n = match !grafite_status with [] -> exit n | grafite_status::_ -> - let baseuri = GrafiteTypes.get_baseuri grafite_status in + let baseuri = grafite_status#baseuri in LibraryClean.clean_baseuris ~verbose:false [baseuri]; exit n @@ -239,10 +239,9 @@ let main () = else begin let baseuri = - GrafiteTypes.get_baseuri - (match !grafite_status with - [] -> assert false - | s::_ -> s) + (match !grafite_status with + [] -> assert false + | s::_ -> s)#baseuri in let moo_fname = LibraryMisc.obj_file_of_baseuri -- 2.39.2