equal
deleted
inserted
replaced
38 { |
38 { |
39 val buffer = text_area.getBuffer |
39 val buffer = text_area.getBuffer |
40 val caret_line = text_area.getCaretLine |
40 val caret_line = text_area.getCaretLine |
41 val caret = text_area.getCaretPosition |
41 val caret = text_area.getCaretPosition |
42 |
42 |
43 Isabelle.session_syntax() match { |
43 Isabelle.buffer_syntax(text_area.getBuffer) match { |
44 case Some(syntax) => |
44 case Some(syntax) => |
45 val limit = PIDE.options.value.int("jedit_structure_limit") max 0 |
45 val limit = PIDE.options.value.int("jedit_structure_limit") max 0 |
46 |
46 |
47 def is_command_kind(token: Token, pred: String => Boolean): Boolean = |
47 def is_command_kind(token: Token, pred: String => Boolean): Boolean = |
48 syntax.keywords.is_command_kind(token, pred) |
48 syntax.keywords.is_command_kind(token, pred) |
141 |
141 |
142 def selectMatch(text_area: TextArea) |
142 def selectMatch(text_area: TextArea) |
143 { |
143 { |
144 def get_span(offset: Text.Offset): Option[Text.Range] = |
144 def get_span(offset: Text.Offset): Option[Text.Range] = |
145 for { |
145 for { |
146 syntax <- Isabelle.session_syntax() |
146 syntax <- Isabelle.buffer_syntax(text_area.getBuffer) |
147 span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset) |
147 span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset) |
148 } yield span.range |
148 } yield span.range |
149 |
149 |
150 find_pair(text_area) match { |
150 find_pair(text_area) match { |
151 case Some((r1, r2)) => |
151 case Some((r1, r2)) => |