]> matita.cs.unibo.it Git - helm.git/commitdiff
- support for comments added in mathql_db_map.txt
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 30 Jul 2003 15:45:03 +0000 (15:45 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 30 Jul 2003 15:45:03 +0000 (15:45 +0000)
helm/ocaml/mathql_interpreter/mQIMap.ml

index 20923f982705f9ea46d391f7cc21754a713aadac..341ebd310490802e786991c7082d2d1b48207aca 100644 (file)
@@ -48,8 +48,10 @@ let read_map () =
       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