]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/parser.ml
Command line arguments to ./a.out
[fireball-separation.git] / ocaml / parser.ml
index ac692516a68cc1786e4b46c08435992236b8e478..726d076357f77539add48e69cdb04b9efb975367 100644 (file)
@@ -182,7 +182,9 @@ prerr_endline (s);
   if line = "" then chr, name, div, conv, ps else\r
   let rec aux' chr line =\r
    if chr = "#"\r
-    then chr, line, div, conv, ps\r
+    then chr, name, div, conv, ps\r
+   else if chr = "$"\r
+    then "#", line, div, conv, ps\r
    else if chr = "D"\r
     then chr, name, line, conv, ps\r
    else if chr = "C"\r
@@ -246,3 +248,18 @@ let ps = List.map (
  ) ps in\r
  name, div, conv, ps, free\r
 ;;\r
+\r
+\r
+let from_file path =\r
+ let lines = ref [] in\r
+ let chan = open_in path in\r
+ let _ = try\r
+  while true; do\r
+    lines := input_line chan :: !lines\r
+  done\r
+ with End_of_file ->\r
+  close_in chan in\r
+ let txt = String.concat "\n" (List.rev !lines) in\r
+ let problems = Str.split (Str.regexp "\\$") txt in\r
+ List.map problem_of_string (List.tl (List.map ((^) "$") problems))\r
+;;\r