equal
deleted
inserted
replaced
86 catch { case ERROR(_) => None } |
86 catch { case ERROR(_) => None } |
87 Line.Node_Range(File.platform_url(name), |
87 Line.Node_Range(File.platform_url(name), |
88 opt_text match { |
88 opt_text match { |
89 case Some(text) if range.start > 0 => |
89 case Some(text) if range.start > 0 => |
90 val chunk = Symbol.Text_Chunk(text) |
90 val chunk = Symbol.Text_Chunk(text) |
91 val doc = Line.Document(text, model.doc.text_length) |
91 val doc = Line.Document(text, resources.text_length) |
92 doc.range(chunk.decode(range)) |
92 doc.range(chunk.decode(range)) |
93 case _ => |
93 case _ => |
94 Line.Range(Line.Position((line1 - 1) max 0)) |
94 Line.Range(Line.Position((line1 - 1) max 0)) |
95 }) |
95 }) |
96 } |
96 } |