81 |
|
|
82 |
def jlinkstr(jlink, box, RoughEdge=1): |
def jlinkstr(jlink, box, RoughEdge=1): |
83 |
if jlink != None: |
if jlink != None: |
84 |
|
#trimming jlink to comparable |
85 |
|
name = jlink |
86 |
|
if name.rfind("#") != -1: |
87 |
|
name = name[0:name.rfind("#")] |
88 |
|
if name.endswith(".html"): name = name[0:len(name)-5] |
89 |
|
if name.endswith(".gen"): name = name[0:len(name)-4] |
90 |
|
|
91 |
|
#Marking "Broken link" if file not found |
92 |
if settings.has_key('path'): |
if settings.has_key('path'): |
93 |
slash = settings['path'].rfind("/") |
slash = settings['path'].rfind("/") |
94 |
if slash != -1: |
if slash != -1: |
100 |
if not os.path.isfile(path): |
if not os.path.isfile(path): |
101 |
# print path |
# print path |
102 |
return 'showlinkerror("'+jlink+'", ('+box+'));' |
return 'showlinkerror("'+jlink+'", ('+box+'));' |
103 |
|
else: |
104 |
|
file = open(path) |
105 |
|
title = re.compile('<title>([^<]*)</title>') |
106 |
|
title = title.findall(file.read()) |
107 |
|
file.close() |
108 |
|
if len(title) > 0: title = title[0] |
109 |
|
else: title = jlink |
110 |
|
titles[jlink] = title |
111 |
|
|
112 |
|
|
113 |
""" If focus is set and 'focus' matches, focus jlink. """ |
""" If focus is set and 'focus' matches, focus jlink. """ |
|
#trimming jlink to comparable |
|
|
name = jlink |
|
|
if name.rfind("#") != -1: |
|
|
name = name[0:name.rfind("#")] |
|
|
if name.endswith(".html"): name = name[0:len(name)-5] |
|
|
if name.endswith(".gen"): name = name[0:len(name)-4] |
|
114 |
#comparing |
#comparing |
115 |
if settings.has_key('focus') and (\ |
if settings.has_key('focus') and (\ |
116 |
settings['focus'].find("_"+name.replace(".", "_")+".") != -1 or \ |
settings['focus'].find("_"+name.replace(".", "_")+".") != -1 or \ |