From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 14 Jul 2017 18:32:20 +0000 (+0200)
Subject: Fixed problems separator in parser: now it is $
X-Git-Tag: weak-reduction-separation~32
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4f1d4ac662d6aeb8e63ddcd4575f9ef6313a565b;p=fireball-separation.git

Fixed problems separator in parser: now it is $

A separable problem's label may start with '!', a not separable's with '?'

(cherry picked from commit 71f8eb7befd85ff4911658136597b41ed177ff8c)
---

diff --git a/ocaml/parser.ml b/ocaml/parser.ml
index a1a9d95..15e2a6a 100644
--- a/ocaml/parser.ml
+++ b/ocaml/parser.ml
@@ -175,7 +175,9 @@ prerr_endline (s);
   if line = "" then chr, name, div, conv, ps else
   let rec aux' chr line =
    if chr = "#"
-    then chr, line, div, conv, ps
+    then chr, name, div, conv, ps
+   else if chr = "$"
+    then "#", line, div, conv, ps
    else if chr = "D"
     then chr, name, line, conv, ps
    else if chr = "C"
@@ -235,6 +237,6 @@ let from_file path =
  with End_of_file ->
   close_in chan in
  let txt = String.concat "\n" (List.rev !lines) in
- let problems = Str.split (Str.regexp "\r?\n\r?\n\\#") txt in
- List.map problem_of_string problems
+ let problems = Str.split (Str.regexp "\\$") txt in
+ List.map problem_of_string (List.tl (List.map ((^) "$") problems))
 ;;