michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(bin/ltags): handle recursor specially in tags generation

Browse source 
fix #197
This commit is contained in:
Soonho Kong 2014-09-15 15:17:46 -07:00
parent 8899ded46b
commit a803b8fd8d
1 changed files with 12 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
bin/ltags
View file

@ -31,11 +31,17 @@ def parse_arg(argv):
args = parser.parse_args(argv) args = parser.parse_args(argv)
return args return args
def get_short_name(id): def get_short_name(item):
last_pos_of_dot = id.rfind('.') category = item['category']
if last_pos_of_dot >= 0: declname = item['declname']
return id[last_pos_of_dot+1:] names = declname.split(".")
return id if category == "d":
kind = item['kind']
# For instance, for the recursor "nat.rec", this function should return "nat"
if kind == "recursor" and len(names) >= 2:
return names[-2]
# Normally, it returns the last part of hierarchical name
return names[-1]
def build_line_to_byteoffset_map(ilean_filename): def build_line_to_byteoffset_map(ilean_filename):
"""Given a .ilean filename, return a mapping from a line number to the """Given a .ilean filename, return a mapping from a line number to the
@ -68,7 +74,7 @@ def convert_position_to_etag_style(info):
linenum = item['linenum'] linenum = item['linenum']
col = item['col'] col = item['col']
item['offset'] = line_to_byteoffset[linenum] + col item['offset'] = line_to_byteoffset[linenum] + col
item['prefix'] = contents[linenum][:col] + get_short_name(item['declname']) item['prefix'] = contents[linenum][:col] + get_short_name(item)
def extract_info_from_ilean(ilean_file, decl_dict): def extract_info_from_ilean(ilean_file, decl_dict):
info = [] info = []