lex-lex
commented
5 years ago This is because it returns an object {"error":"Cannot parse formula 2 out of 2 formulae: ~a - Error: Error: \n-- PARSING FAILED --------------------------------------------------\n\n> 1 | ~a\n | ^\n\nExpected one of the following: \n\n'(', 'false', 'true', /[A-Z][a-zA-Z_\\d]*/, /[a-z][a-zA-Z_\\d]*/\n"} while the front end expects the usual object containing message and type.
When there is an error in the formalization (i.e. try to use the following syntactically incorrect term - '~a'), saving works fine but when trying to run a consistency check (this is the part that the JSON parsing into DL* and then into MleanCoP syntax is taking place here), one of the parsers encounter an error. The message is though - Unexpected error: Error: Request failed with status code 400