javascript:(function(){
    var path = location.pathname.replace(/^\//,"").replace(/\.html$/,"");
    var as =document.getElementsByTagName("a");
    for (i in as) { 
        var l = as[i]; 
        if (l.id && l.classList.length == 0 ){
            var dlink   = path + "#" + l.id;
            l.innerHTML = "<b>" + path + "#[doc://"+dlink+"]</b><br>"; 
            l.href      = "#" + l.id 
        } 
    }
})()