diff options
Diffstat (limited to 'src/parse.c')
| -rw-r--r-- | src/parse.c | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/parse.c b/src/parse.c index 830f9c5..cae66a0 100644 --- a/src/parse.c +++ b/src/parse.c @@ -61,9 +61,14 @@ line_t parse_line(char* content) { } c++; } + /* find the proposition and justification */ + int* seek = calloc(sizeof(int), 1); + prop_t prop = parse_proposition(init_tokenset(ts.tokens + indent, c - indent), seek, 0); + just_t just = parse_justification(init_tokenset(ts.tokens + c + 1, ts.count - (c + 1))); + free(seek); /* determine the ID of the scope we are working on */ scope_t thisScope; - if (indent > lastScope.depth) { + if (indent > lastScope.depth || just.rule == ASSUMPTION_R) { scopes++; scope_t* lsp = malloc(sizeof(scope_t)); *lsp = lastScope; @@ -81,12 +86,7 @@ line_t parse_line(char* content) { thisScope = lastScope; } lastScope = thisScope; - /* find the proposition and justification */ - int* seek = calloc(sizeof(int), 1); - prop_t prop = parse_proposition(init_tokenset(ts.tokens + indent, c - indent), seek, 0); - just_t just = parse_justification(init_tokenset(ts.tokens + c + 1, ts.count - (c + 1))); - free(seek); - if ((just.rule != ASSUMPTION_R && isNewIndent) || (just.rule == ASSUMPTION_R && !isNewIndent)) { + if ((just.rule != ASSUMPTION_R && isNewIndent) || (just.rule == ASSUMPTION_R && !isNewIndent) || (just.rule == PREMISE_R && indent != 0)) { just.rule = ERR_R; } return init_line(thisScope, prop, just); |