50 Isabelle.buffer_syntax(buffer) match { |
50 Isabelle.buffer_syntax(buffer) match { |
51 case Some(syntax) if buffer.isInstanceOf[Buffer] => |
51 case Some(syntax) if buffer.isInstanceOf[Buffer] => |
52 val keywords = syntax.keywords |
52 val keywords = syntax.keywords |
53 val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true) |
53 val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true) |
54 |
54 |
55 def head_token(line: Int): Option[Token] = |
55 val indent_size = buffer.getIndentSize |
56 nav.iterator(line, 1).toStream.headOption.map(_.info) |
56 |
|
57 |
|
58 def line_indent(line: Int): Int = |
|
59 if (line < 0 || line >= buffer.getLineCount) 0 |
|
60 else buffer.getCurrentIndentForLine(line, null) |
|
61 |
|
62 def line_head(line: Int): Option[Text.Info[Token]] = |
|
63 nav.iterator(line, 1).toStream.headOption |
57 |
64 |
58 def head_is_quasi_command(line: Int): Boolean = |
65 def head_is_quasi_command(line: Int): Boolean = |
59 head_token(line) match { |
66 line_head(line) match { |
60 case None => false |
67 case None => false |
61 case Some(tok) => keywords.is_quasi_command(tok) |
68 case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok) |
62 } |
69 } |
63 |
70 |
64 def prev_command: Option[Token] = |
71 def prev_command: Option[Token] = |
65 nav.reverse_iterator(prev_line, 1). |
72 nav.reverse_iterator(prev_line, 1). |
66 collectFirst({ case Text.Info(_, tok) if tok.is_command => tok }) |
73 collectFirst({ case Text.Info(_, tok) if tok.is_command => tok }) |
70 |
77 |
71 def prev_line_span: Iterator[Token] = |
78 def prev_line_span: Iterator[Token] = |
72 nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_command) |
79 nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_command) |
73 |
80 |
74 |
81 |
75 def line_indent(line: Int): Int = |
82 val script_indent: Text.Range => Int = |
76 if (line < 0 || line >= buffer.getLineCount) 0 |
83 { |
77 else buffer.getCurrentIndentForLine(line, null) |
84 val opt_rendering: Option[Rendering] = |
78 |
85 if (PIDE.options.value.bool("jedit_indent_script")) |
79 val indent_size = buffer.getIndentSize |
86 GUI_Thread.now { |
|
87 (for { |
|
88 text_area <- JEdit_Lib.jedit_text_areas(buffer) |
|
89 doc_view <- PIDE.document_view(text_area) |
|
90 } yield doc_view.get_rendering).toStream.headOption |
|
91 } |
|
92 else None |
|
93 val limit = PIDE.options.value.int("jedit_indent_script_limit") |
|
94 (range: Text.Range) => |
|
95 opt_rendering match { |
|
96 case Some(rendering) => (rendering.indentation(range) min limit) max 0 |
|
97 case None => 0 |
|
98 } |
|
99 } |
80 |
100 |
81 def indent_indent(tok: Token): Int = |
101 def indent_indent(tok: Token): Int = |
82 if (keywords.is_command(tok, keyword_open)) indent_size |
102 if (keywords.is_command(tok, keyword_open)) indent_size |
83 else if (keywords.is_command(tok, keyword_close)) - indent_size |
103 else if (keywords.is_command(tok, keyword_close)) - indent_size |
84 else 0 |
104 else 0 |
100 |
120 |
101 def indent_structure: Int = |
121 def indent_structure: Int = |
102 nav.reverse_iterator(current_line - 1).scanLeft((0, false))( |
122 nav.reverse_iterator(current_line - 1).scanLeft((0, false))( |
103 { case ((ind, _), Text.Info(range, tok)) => |
123 { case ((ind, _), Text.Info(range, tok)) => |
104 val ind1 = ind + indent_indent(tok) |
124 val ind1 = ind + indent_indent(tok) |
105 if (tok.is_command) { |
125 if (tok.is_command && !keywords.is_command(tok, Keyword.PRF_SCRIPT == _)) { |
106 val line = buffer.getLineOfOffset(range.start) |
126 val line = buffer.getLineOfOffset(range.start) |
107 if (head_token(line) == Some(tok)) |
127 line_head(line) match { |
108 (ind1 + indent_offset(tok) + line_indent(line), true) |
128 case Some(info) if info.info == tok => |
109 else (ind1, false) |
129 (ind1 + indent_offset(tok) + line_indent(line), true) |
|
130 case _ => (ind1, false) |
|
131 } |
110 } |
132 } |
111 else (ind1, false) |
133 else (ind1, false) |
112 }).collectFirst({ case (i, true) => i }).getOrElse(0) |
134 }).collectFirst({ case (i, true) => i }).getOrElse(0) |
113 |
135 |
114 def nesting(it: Iterator[Token], open: Token => Boolean, close: Token => Boolean): Int = |
136 def nesting(it: Iterator[Token], open: Token => Boolean, close: Token => Boolean): Int = |
117 def indent_begin: Int = |
139 def indent_begin: Int = |
118 (nesting(nav.iterator(current_line - 1, 1).map(_.info), _.is_begin, _.is_end) max 0) * |
140 (nesting(nav.iterator(current_line - 1, 1).map(_.info), _.is_begin, _.is_end) max 0) * |
119 indent_size |
141 indent_size |
120 |
142 |
121 val indent = |
143 val indent = |
122 head_token(current_line) match { |
144 line_head(current_line) match { |
123 case None => indent_structure + indent_brackets + indent_extra |
145 case None => indent_structure + indent_brackets + indent_extra |
124 case Some(tok) => |
146 case Some(Text.Info(range, tok)) => |
125 if (keywords.is_before_command(tok) || |
147 if (keywords.is_before_command(tok) || |
126 keywords.is_command(tok, Keyword.theory)) indent_begin |
148 keywords.is_command(tok, Keyword.theory)) indent_begin |
127 else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok) |
149 else if (keywords.is_command(tok, Keyword.PRF_SCRIPT == _)) |
|
150 indent_structure + script_indent(range) |
|
151 else if (tok.is_command) |
|
152 indent_structure + indent_begin - indent_offset(tok) |
128 else { |
153 else { |
129 prev_command match { |
154 prev_command match { |
130 case None => |
155 case None => |
131 val extra = |
156 val extra = |
132 (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { |
157 (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { |