equal
deleted
inserted
replaced
110 if String.isPrefix successN line then (true, NONE) |
110 if String.isPrefix successN line then (true, NONE) |
111 else if String.isPrefix failureN line then (false, |
111 else if String.isPrefix failureN line then (false, |
112 if size line > size failureN then |
112 if size line > size failureN then |
113 String.extract (line, size failureN, NONE) |
113 String.extract (line, size failureN, NONE) |
114 |> YXML.parse_body |
114 |> YXML.parse_body |
115 |> Term_XML.Decode.term |
115 |> Term_XML.Decode.term_raw |
116 |> dest_tuples |
116 |> dest_tuples |
117 |> SOME |
117 |> SOME |
118 else NONE) |
118 else NONE) |
119 else raise Fail ("Cannot parse result of evaluation:\n" ^ line) |
119 else raise Fail ("Cannot parse result of evaluation:\n" ^ line) |
120 |
120 |