src/Pure/PIDE/rendering.scala
changeset 64648 5d7f741aaccb
parent 64622 529bbb8977c7
child 64654 31b681e38c70
     1.1 --- a/src/Pure/PIDE/rendering.scala	Wed Dec 21 21:17:44 2016 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Wed Dec 21 21:18:37 2016 +0100
     1.3 @@ -46,6 +46,11 @@
     1.4        resources.append(snapshot.node_name.master_dir, Path.explode(name))
     1.5      else name
     1.6  
     1.7 +  def resolve_file_url(name: String): String =
     1.8 +    if (Path.is_valid(name))
     1.9 +      "file://" + resources.append(snapshot.node_name.master_dir, Path.explode(name))
    1.10 +    else name
    1.11 +
    1.12  
    1.13    /* tooltips */
    1.14