| changeset 73340 | 0ffcad1f6130 |
| parent 70253 | cb334a92a4db |
| child 75393 | 87ebf5a50283 |
| 73339:9efdebe24c65 | 73340:0ffcad1f6130 |
|---|---|
78 } |
78 } |
79 |
79 |
80 |
80 |
81 /* open browser */ |
81 /* open browser */ |
82 |
82 |
83 def open_browser(view: View) |
83 def open_browser(view: View): Unit = |
84 { |
84 { |
85 val path = |
85 val path = |
86 PIDE.maybe_snapshot(view) match { |
86 PIDE.maybe_snapshot(view) match { |
87 case None => "" |
87 case None => "" |
88 case Some(snapshot) => |
88 case Some(snapshot) => |