equal
deleted
inserted
replaced
84 nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command) |
84 nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command) |
85 |
85 |
86 |
86 |
87 val script_indent: Text.Info[Token] => Int = |
87 val script_indent: Text.Info[Token] => Int = |
88 { |
88 { |
89 val opt_rendering: Option[Rendering] = |
89 val opt_rendering: Option[JEdit_Rendering] = |
90 if (PIDE.options.value.bool("jedit_indent_script")) |
90 if (PIDE.options.value.bool("jedit_indent_script")) |
91 GUI_Thread.now { |
91 GUI_Thread.now { |
92 (for { |
92 (for { |
93 text_area <- JEdit_Lib.jedit_text_areas(buffer) |
93 text_area <- JEdit_Lib.jedit_text_areas(buffer) |
94 doc_view <- PIDE.document_view(text_area) |
94 doc_view <- PIDE.document_view(text_area) |