X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQIMap.ml;h=a5b6654c88aeee7309ba58806b3924fe3c56a5bc;hb=b1bad322d0daf6c25f95a82c4349f057a753ab7c;hp=20923f982705f9ea46d391f7cc21754a713aadac;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/ocaml/mathql_interpreter/mQIMap.ml b/helm/ocaml/mathql_interpreter/mQIMap.ml index 20923f982..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,22 +36,19 @@ type pg_tables = (bool * string) list type pg_alias = (string * string) list -let empty_map () = "", [], [] +let empty_map () = [], [] let read_map () = - let default_map = "mathql_db_map.txt" in - let map = - try Sys.getenv "MATHQL_DB_MAP" - with Not_found -> default_map - in + 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 | [] -> aux r s + | "#" :: _ -> aux r s | t :: "<-" :: p -> aux ((p, (false, t, None)) :: r) s | t :: c :: "<-" :: p -> aux ((p, (false, t, Some c)) :: r) s + | t :: "<+" :: p -> aux ((p, (true, t, None)) :: r) s | t :: c :: "<+" :: p -> aux ((p, (true, t, Some c)) :: r) s | [a; "->"; t] -> aux r ((a, t) :: s) | ["->"] -> r, s @@ -57,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