equal
deleted
inserted
replaced
81 |
81 |
82 def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range) |
82 def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range) |
83 : Option[Line.Node_Range] = |
83 : Option[Line.Node_Range] = |
84 { |
84 { |
85 for { |
85 for { |
86 name <- resources.source_file(source_name) |
86 platform_path <- resources.source_file(source_name) |
87 file <- |
87 file <- |
88 (try { Some(new JFile(name).getCanonicalFile) } |
88 (try { Some(new JFile(platform_path).getCanonicalFile) } |
89 catch { case ERROR(_) => None }) |
89 catch { case ERROR(_) => None }) |
90 } |
90 } |
91 yield { |
91 yield { |
92 val opt_text = |
|
93 try { Some(File.read(file)) } // FIXME content from resources/models |
|
94 catch { case ERROR(_) => None } |
|
95 Line.Node_Range(file.getPath, |
92 Line.Node_Range(file.getPath, |
96 opt_text match { |
93 resources.get_file_content(file) match { |
97 case Some(text) if range.start > 0 => |
94 case Some(text) if range.start > 0 => |
98 val chunk = Symbol.Text_Chunk(text) |
95 val chunk = Symbol.Text_Chunk(text) |
99 val doc = Line.Document(text, resources.text_length) |
96 val doc = Line.Document(text, resources.text_length) |
100 doc.range(chunk.decode(range)) |
97 doc.range(chunk.decode(range)) |
101 case _ => |
98 case _ => |