X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_engine%2FgrafiteSync.ml;fp=helm%2Focaml%2Fgrafite_engine%2FgrafiteSync.ml;h=0000000000000000000000000000000000000000;hb=55b82bd235d82ff7f0a40d980effe1efde1f5073;hp=37a3132e70e232c04b1437f6613d36c6983a02ef;hpb=771ee8b9d122fa963881c876e86f90531bb7434f;p=helm.git

diff --git a/helm/ocaml/grafite_engine/grafiteSync.ml b/helm/ocaml/grafite_engine/grafiteSync.ml
deleted file mode 100644
index 37a3132e7..000000000
--- a/helm/ocaml/grafite_engine/grafiteSync.ml
+++ /dev/null
@@ -1,74 +0,0 @@
-(* Copyright (C) 2004-2005, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open Printf
-
-let add_obj ~basedir uri obj status =
- let lemmas = LibrarySync.add_obj uri obj basedir in
-  {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects},
-   lemmas
-
-let add_coercion ~basedir ~add_composites status uri =
- let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in
-  {status with GrafiteTypes.coercions = uri :: status.GrafiteTypes.coercions},
-   compounds
- 
-module OrderedUri =
-struct
-  type t = UriManager.uri * string
-  let compare (u1, _) (u2, _) = UriManager.compare u1 u2
-end
-
-module UriSet = Set.Make (OrderedUri)
-
-  (** @return l2 \ l1 *)
-let uri_list_diff l2 l1 =
-  let module S = UriManager.UriSet in
-  let s1 = List.fold_left (fun set uri -> S.add uri set) S.empty l1 in
-  let s2 = List.fold_left (fun set uri -> S.add uri set) S.empty l2 in
-  let diff = S.diff s2 s1 in
-  S.fold (fun uri uris -> uri :: uris) diff []
-
-let time_travel ~present ~past =
-  let objs_to_remove =
-   uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in
-  let coercions_to_remove =
-   uri_list_diff present.GrafiteTypes.coercions past.GrafiteTypes.coercions
-  in
-   List.iter (fun uri -> LibrarySync.remove_coercion uri) coercions_to_remove;
-   List.iter LibrarySync.remove_obj objs_to_remove
-
-let init () =
-  LibrarySync.remove_all_coercions ();
-  LibraryObjects.reset_defaults ();
-  {
-    GrafiteTypes.moo_content_rev = [];
-    proof_status = GrafiteTypes.No_proof;
-    options = GrafiteTypes.no_options;
-    objects = [];
-    coercions = [];
-  }