]> matita.cs.unibo.it Git - helm.git/commitdiff
added is_blank_line facility to match line that should be ignored in
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 25 Feb 2003 14:05:50 +0000 (14:05 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 25 Feb 2003 14:05:50 +0000 (14:05 +0000)
indexes

helm/http_getter/http_getter_common.ml
helm/http_getter/http_getter_common.mli

index 40e5648ca2379ece56bbd69acdb025fff3f3b303..b6933218ebda79735a897647aded1ca20d7346ab 100644 (file)
@@ -41,6 +41,11 @@ let is_nuprl_uri uri = Pcre.pmatch ~pat:"^nuprl:" uri
 let is_rdf_uri uri = Pcre.pmatch ~pat:"^helm:rdf(.*):(.*)//(.*)" uri
 let is_xsl_uri uri = Pcre.pmatch ~pat:"^\\w+\\.xsl" uri
 
+let is_blank_line =
+  let blank_line_RE = Pcre.regexp "(^#)|(^\\s*$)" in
+  fun line ->
+    Pcre.pmatch ~rex:blank_line_RE line
+
 let rec http_getter_uri_of_string = function
   | uri when is_rdf_uri uri ->
       (match Pcre.split ~pat:"//" uri with
index 05f495f2f6efeb107355ae43ef847b36d8b75913..711a5713d9f6fa3d195e810e5c2c18d16d758dde 100644 (file)
@@ -36,6 +36,9 @@ val is_nuprl_uri: string -> bool
 val is_rdf_uri: string -> bool
 val is_xsl_uri: string -> bool
 
+  (** true on blanks-only and #-commented lines, false otherwise *)
+val is_blank_line: string -> bool
+
 val http_getter_uri_of_string: string -> http_getter_uri
 
 val patch_xml : string -> string