X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQIMap.ml;h=a5b6654c88aeee7309ba58806b3924fe3c56a5bc;hb=f553eb12e42b11d37dbf1ae3f8ceb859a875df98;hp=ed02524cce9ee56994d7351ddc3f389e01343dc7;hpb=d9b746b8c3a6f62d874329c425ea444969af5576;p=helm.git diff --git a/helm/ocaml/mathql_interpreter/mQIMap.ml b/helm/ocaml/mathql_interpreter/mQIMap.ml index ed02524cc..a5b6654c8 100644 --- a/helm/ocaml/mathql_interpreter/mQIMap.ml +++ b/helm/ocaml/mathql_interpreter/mQIMap.ml @@ -26,6 +26,8 @@ (* AUTOR: Ferruccio Guidi *) +(* $Id$ *) + module U = MQueryUtil type pg_map = (MathQL.path * (bool * string * string option)) list @@ -34,12 +36,11 @@ type pg_tables = (bool * string) list type pg_alias = (string * string) list -let empty_map () = "", [], [] +let empty_map () = [], [] let read_map () = let map = Helm_registry.get "mathql_interpreter.db_map" in let ich = open_in map in - let pgs = input_line ich in let rec aux r s = let d = input_line ich in match Str.split (Str.regexp "[ \t]+") d with @@ -55,7 +56,7 @@ let read_map () = in let pgm, pga = aux [] [] in close_in ich; - pgs, pgm, pga + pgm, pga let comp c1 c2 = match c1, c2 with | (_, t1), (_, t2) when t1 < t2 -> U.Lt