164 ((structure.span_depth, structure.after_span_depth) /: tokens) { |
164 ((structure.span_depth, structure.after_span_depth) /: tokens) { |
165 case ((x, y), tok) => |
165 case ((x, y), tok) => |
166 if (tok.is_command) { |
166 if (tok.is_command) { |
167 if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1) |
167 if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1) |
168 else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0) |
168 else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0) |
|
169 else if (tok.is_command_kind(keywords, Keyword.PRF_BLOCK == _)) (y + 2, y + 1) |
|
170 else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 3) |
169 else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1) |
171 else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1) |
170 else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1) |
172 else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1) |
171 else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0) |
173 else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0) |
172 else (x, y) |
174 else (x, y) |
173 } |
175 } |