equal
deleted
inserted
replaced
81 |
81 |
82 def node_perspective(): Text.Perspective = |
82 def node_perspective(): Text.Perspective = |
83 { |
83 { |
84 Swing_Thread.require() |
84 Swing_Thread.require() |
85 |
85 |
86 PIDE.execution_range() match { |
86 if (PIDE.continuous_checking) { |
87 case PIDE.Execution_Range.ALL => Text.Perspective.full |
87 Text.Perspective( |
88 case PIDE.Execution_Range.NONE => Text.Perspective.empty |
88 for { |
89 case PIDE.Execution_Range.VISIBLE => |
89 doc_view <- PIDE.document_views(buffer) |
90 Text.Perspective( |
90 range <- doc_view.perspective().ranges |
91 for { |
91 } yield range) |
92 doc_view <- PIDE.document_views(buffer) |
92 } |
93 range <- doc_view.perspective().ranges |
93 else Text.Perspective.empty |
94 } yield range) |
|
95 } |
|
96 } |
94 } |
97 |
95 |
98 |
96 |
99 /* edits */ |
97 /* edits */ |
100 |
98 |