156 |
refer_names[id] = random_var() |
refer_names[id] = random_var() |
157 |
|
|
158 |
element = mptitle(refer_names[id], [title], |
element = mptitle(refer_names[id], [title], |
159 |
[[['link'], [target+'#'+diagram]]]) |
[[['link'], [target]]]) |
160 |
if id == len(refers)-1: |
if id == len(refers)-1: |
161 |
context_menu += "\tdraw ulcorner(bbox(currentpicture))+(0,10) -- urcorner(bbox(currentpicture))+(0,10) withpen pencircle scaled 1.5pt;\n" |
context_menu += "\tdraw ulcorner(bbox(currentpicture))+(0,10) -- urcorner(bbox(currentpicture))+(0,10) withpen pencircle scaled 1.5pt;\n" |
162 |
context_menu += element.setup_code() |
context_menu += element.setup_code() |
344 |
self.target = slashify(relative_path(config.working_directory, config.mp_directory))+diagram+config.midfix+'.png' |
self.target = slashify(relative_path(config.working_directory, config.mp_directory))+diagram+config.midfix+'.png' |
345 |
if self.target.endswith('.png'): |
if self.target.endswith('.png'): |
346 |
target = '_plain' |
target = '_plain' |
347 |
else: target = '_top' |
diagram = '' |
348 |
|
else: |
349 |
return """<area href="%s" shape="rect" coords="%s" target="%s" title="%s" alt="%s" />""" \ |
target = '_top' |
350 |
% (self.target, |
diagram = '#'+diagram |
351 |
|
|
352 |
|
return """<area href="%s%s" shape="rect" coords="%s" target="%s" title="%s" alt="%s" />""" \ |
353 |
|
% (self.target, diagram, |
354 |
",".join(["%s"%(int(c*scale)) for c in self.corners]), |
",".join(["%s"%(int(c*scale)) for c in self.corners]), |
355 |
target, |
target, |
356 |
self.title, |
self.title, |