]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_common.ml
added is_blank_line facility to match line that should be ignored in
[helm.git] / helm / http_getter / http_getter_common.ml
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