equal
deleted
inserted
replaced
66 collectFirst({ case Text.Info(_, tok) if tok.is_command => tok }) |
66 collectFirst({ case Text.Info(_, tok) if tok.is_command => tok }) |
67 |
67 |
68 def prev_span: Iterator[Token] = |
68 def prev_span: Iterator[Token] = |
69 nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_command) |
69 nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_command) |
70 |
70 |
|
71 def prev_line_span: Iterator[Token] = |
|
72 nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_command) |
|
73 |
71 |
74 |
72 def line_indent(line: Int): Int = |
75 def line_indent(line: Int): Int = |
73 if (line < 0 || line >= buffer.getLineCount) 0 |
76 if (line < 0 || line >= buffer.getLineCount) 0 |
74 else buffer.getCurrentIndentForLine(line, null) |
77 else buffer.getCurrentIndentForLine(line, null) |
75 |
78 |
81 else 0 |
84 else 0 |
82 |
85 |
83 def indent_offset(tok: Token): Int = |
86 def indent_offset(tok: Token): Int = |
84 if (keywords.is_command(tok, Keyword.proof_enclose) || tok.is_begin) indent_size |
87 if (keywords.is_command(tok, Keyword.proof_enclose) || tok.is_begin) indent_size |
85 else 0 |
88 else 0 |
|
89 |
|
90 def indent_brackets: Int = |
|
91 (0 /: prev_line_span)( |
|
92 { case (i, tok) => |
|
93 if (tok.is_open_bracket) i + indent_size |
|
94 else if (tok.is_close_bracket) i - indent_size |
|
95 else i }) |
86 |
96 |
87 def indent_extra: Int = |
97 def indent_extra: Int = |
88 if (prev_span.exists(keywords.is_quasi_command(_))) indent_size |
98 if (prev_span.exists(keywords.is_quasi_command(_))) indent_size |
89 else 0 |
99 else 0 |
90 |
100 |
108 (nesting(nav.iterator(current_line - 1, 1).map(_.info), _.is_begin, _.is_end) max 0) * |
118 (nesting(nav.iterator(current_line - 1, 1).map(_.info), _.is_begin, _.is_end) max 0) * |
109 indent_size |
119 indent_size |
110 |
120 |
111 val indent = |
121 val indent = |
112 head_token(current_line) match { |
122 head_token(current_line) match { |
113 case None => indent_structure + indent_extra |
123 case None => indent_structure + indent_brackets + indent_extra |
114 case Some(tok) => |
124 case Some(tok) => |
115 if (keywords.is_before_command(tok) || |
125 if (keywords.is_before_command(tok) || |
116 keywords.is_command(tok, Keyword.theory)) indent_begin |
126 keywords.is_command(tok, Keyword.theory)) indent_begin |
117 else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok) |
127 else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok) |
118 else { |
128 else { |
122 (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { |
132 (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { |
123 case (true, true) | (false, false) => 0 |
133 case (true, true) | (false, false) => 0 |
124 case (true, false) => - indent_extra |
134 case (true, false) => - indent_extra |
125 case (false, true) => indent_extra |
135 case (false, true) => indent_extra |
126 } |
136 } |
127 line_indent(prev_line) - indent_offset(tok) + extra |
137 line_indent(prev_line) - indent_offset(tok) + indent_brackets + extra |
128 case Some(prev_tok) => |
138 case Some(prev_tok) => |
129 indent_structure - indent_offset(tok) - indent_offset(prev_tok) - |
139 indent_structure - indent_offset(tok) - indent_offset(prev_tok) + |
130 indent_indent(prev_tok) + indent_size |
140 indent_brackets - indent_indent(prev_tok) + indent_size |
131 } |
141 } |
132 } |
142 } |
133 } |
143 } |
134 |
144 |
135 actions.clear() |
145 actions.clear() |