]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Fixed problems separator in parser: now it is $
authoracondolu <andrea.condoluci@unibo.it>
Fri, 14 Jul 2017 18:32:20 +0000 (20:32 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 09:08:58 +0000 (11:08 +0200)
A separable problem's label may start with '!', a not separable's with '?'

(cherry picked from commit 71f8eb7befd85ff4911658136597b41ed177ff8c)

ocaml/parser.ml

index a1a9d95a7dd85f91545009d81c132cfbc49676ef..15e2a6a4e170dd8db1623110d41d9aead5971294 100644 (file)
@@ -175,7 +175,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
@@ -235,6 +237,6 @@ let from_file path =
  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 "\r?\n\r?\n\\#") txt in\r
- List.map problem_of_string problems\r
+ let problems = Str.split (Str.regexp "\\$") txt in\r
+ List.map problem_of_string (List.tl (List.map ((^) "$") problems))\r
 ;;\r