76 else if (keywords.is_command(tok, keyword_close)) - indent_size |
76 else if (keywords.is_command(tok, keyword_close)) - indent_size |
77 else 0 |
77 else 0 |
78 |
78 |
79 def indent_offset(tok: Token): Int = |
79 def indent_offset(tok: Token): Int = |
80 if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size |
80 if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size |
|
81 else if (tok.is_begin) indent_size |
81 else 0 |
82 else 0 |
82 |
83 |
83 def indent_extra: Int = |
84 def indent_extra: Int = |
84 if (prev_span.exists(keywords.is_quasi_command(_))) indent_size |
85 if (prev_span.exists(keywords.is_quasi_command(_))) indent_size |
85 else 0 |
86 else 0 |
95 else (ind1, false) |
96 else (ind1, false) |
96 } |
97 } |
97 else (ind1, false) |
98 else (ind1, false) |
98 }).collectFirst({ case (i, true) => i }).getOrElse(0) |
99 }).collectFirst({ case (i, true) => i }).getOrElse(0) |
99 |
100 |
|
101 def nesting(it: Iterator[Token], open: Token => Boolean, close: Token => Boolean): Int = |
|
102 (0 /: it)({ case (d, tok) => if (open(tok)) d + 1 else if (close(tok)) d - 1 else d }) |
|
103 |
|
104 def indent_begin: Int = |
|
105 (nesting(nav.iterator(current_line - 1, 1).map(_.info), _.is_begin, _.is_end) max 0) * |
|
106 indent_size |
|
107 |
100 val indent = |
108 val indent = |
101 head_token(current_line) match { |
109 head_token(current_line) match { |
102 case None => indent_structure + indent_extra |
110 case None => indent_structure + indent_extra |
103 case Some(tok) => |
111 case Some(tok) => |
104 if (keywords.is_command(tok, Keyword.theory)) 0 |
112 if (keywords.is_command(tok, Keyword.theory)) indent_begin |
105 else if (tok.is_command) indent_structure - indent_offset(tok) |
113 else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok) |
106 else { |
114 else { |
107 prev_command match { |
115 prev_command match { |
108 case None => |
116 case None => |
109 val extra = |
117 val extra = |
110 (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { |
118 (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { |
111 case (true, true) | (false, false) => 0 |
119 case (true, true) | (false, false) => 0 |
112 case (true, false) => - indent_extra |
120 case (true, false) => - indent_extra |
113 case (false, true) => indent_extra |
121 case (false, true) => indent_extra |
114 } |
122 } |
115 line_indent(prev_line) + extra |
123 line_indent(prev_line) - indent_offset(tok) + extra |
116 case Some(prev_tok) => |
124 case Some(prev_tok) => |
117 indent_structure - indent_offset(prev_tok) - |
125 indent_structure - indent_offset(tok) - indent_offset(prev_tok) - |
118 indent_indent(prev_tok) + indent_size |
126 indent_indent(prev_tok) + indent_size |
119 } |
127 } |
120 } |
128 } |
121 } |
129 } |
122 |
130 |