79 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) |
80 : Option[Line.Node_Range] = |
83 : Option[Line.Node_Range] = |
81 { |
84 { |
82 for { |
85 for { |
83 name <- resources.source_file(source_name) |
86 name <- resources.source_file(source_name) |
84 if Path.is_wellformed(name) |
87 file <- |
|
88 (try { Some(new JFile(name).getCanonicalFile) } |
|
89 catch { case ERROR(_) => None }) |
85 } |
90 } |
86 yield { |
91 yield { |
87 val path = Path.explode(name) |
|
88 val opt_text = |
92 val opt_text = |
89 try { Some(File.read(path)) } // FIXME content from resources/models |
93 try { Some(File.read(file)) } // FIXME content from resources/models |
90 catch { case ERROR(_) => None } |
94 catch { case ERROR(_) => None } |
91 Line.Node_Range(File.platform_path(path), |
95 Line.Node_Range(file.getPath, |
92 opt_text match { |
96 opt_text match { |
93 case Some(text) if range.start > 0 => |
97 case Some(text) if range.start > 0 => |
94 val chunk = Symbol.Text_Chunk(text) |
98 val chunk = Symbol.Text_Chunk(text) |
95 val doc = Line.Document(text, resources.text_length) |
99 val doc = Line.Document(text, resources.text_length) |
96 doc.range(chunk.decode(range)) |
100 doc.range(chunk.decode(range)) |