Useless GrafiteTypes.get_baseuri removed.

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index b1cc9d671f5acd17f0fcbf64931c4b220c3e7fd2..192e396af0f2838d0704a53226a9c41699504cf1 100644 (file)
--- 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 9fd40b1c463af8c80b80002c4703b81cdbe1c8c8..959d96f368b4694ce69d9fe97db907eba6ab04f4 100644 (file)
--- 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 c30beead02301170bf77e08cb3ea9dbcf5183867..34e3d09660c0b2e8c7a809d324bdd46a006d7d3d 100644 (file)
--- 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 e9965c4ca130748e0aaf493ad5b93994616142e1..1b4cc5a3cd495042c550710f699a84b1685229ba 100644 (file)
--- 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 6b16891c883621460ccfb5c7133eebd4aa465067..ba4e346969a2757af26c63c9a979f8097b3d77ac 100644 (file)
--- 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 7b5a929cb9466d517acebb527d6ead0baeacf5bb..5272f07a71fd01e48c8242cb77f2bc6657f3fbbc 100644 (file)
--- 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 b52e75741f04b11fb25d9cc08b304aa420bc6cb0..30c7fc9eaf954a9306d0c6c3c0b9884538aa4d85 100644 (file)
--- 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