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

fix(bin/ltags): add option --relative to handle path relatively

Browse source 
Fix #230
This commit is contained in:
Soonho Kong 2014-10-07 15:07:28 -07:00
parent 78e9854bae
commit 4a119a0424
2 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
bin/linja
View file

@ -475,7 +475,7 @@ def make_build_ninja(args):
print >> f, """ command = """, print >> f, """ command = """,
if platform.system() == "Windows": if platform.system() == "Windows":
print >> f, "python ", print >> f, "python ",
print >> f, """"%s" $in """ % (g_ltags_path) print >> f, """"%s" --relative -- $in """ % (g_ltags_path)
print >> f, "build all: phony", print >> f, "build all: phony",
for item in lean_files: for item in lean_files:

11
bin/ltags
View file

@ -24,9 +24,10 @@ def get_ilean_files(directory):
def parse_arg(argv): def parse_arg(argv):
""" Parse arguments """ """ Parse arguments """
parser = argparse.ArgumentParser(description='Process arguments.') parser = argparse.ArgumentParser(description='ltags: tag generator for Lean theorem prover.')
parser.add_argument('--etags', '-e', action='store_true', default=True, help="Generate etags TAGS file.") parser.add_argument('--etags', '-e', action='store_true', default=True, help="Generate etags TAGS file.")
parser.add_argument('--gtags', '-g', action='store_true', default=False, help="Generate gtags files (GTAGS, GRTAGS, GPATH).") # parser.add_argument('--gtags', '-g', action='store_true', default=False, help="Generate gtags files (GTAGS, GRTAGS, GPATH).")
parser.add_argument('--relative', action='store', default=None, const=os.getcwd(), nargs='?', help="Generate relative paths based on the parameter.")
parser.add_argument('files', nargs='*') parser.add_argument('files', nargs='*')
args = parser.parse_args(argv) args = parser.parse_args(argv)
return args return args
@ -76,7 +77,7 @@ def convert_position_to_etag_style(info):
item['offset'] = line_to_byteoffset[linenum] + col item['offset'] = line_to_byteoffset[linenum] + col
item['prefix'] = contents[linenum][:col] + get_short_name(item) 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, args):
info = [] info = []
with open(ilean_file) as f: with open(ilean_file) as f:
for line in f: for line in f:
@ -99,6 +100,8 @@ def extract_info_from_ilean(ilean_file, decl_dict):
item['linenum'] = int(array[2]) item['linenum'] = int(array[2])
item['col'] = int(array[3]) item['col'] = int(array[3])
item['declname'] = array[4] item['declname'] = array[4]
if args.relative and "filename" in item:
item['filename'] = os.path.relpath(item['filename'], args.relative)
info.append(item) info.append(item)
return info return info
@ -212,7 +215,7 @@ def main(argv=None):
info_list = [] info_list = []
decl_dict = {} decl_dict = {}
for ilean_file in ilean_files: for ilean_file in ilean_files:
info = extract_info_from_ilean(ilean_file, decl_dict) info = extract_info_from_ilean(ilean_file, decl_dict, args)
if info: if info:
convert_position_to_etag_style(info) convert_position_to_etag_style(info)
info_list.append(info) info_list.append(info)