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

refactor: rename ltags => leantags

Browse source 
fix #394
This commit is contained in:
Soonho Kong 2015-01-18 13:44:22 +09:00
parent edcc92d9c7
commit 901c9bf67a
4 changed files with 23 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
bin/ltags → bin/leantags
View file

@ -24,7 +24,7 @@ def get_ilean_files(directory):
def parse_arg(argv):
""" Parse arguments """
parser = argparse.ArgumentParser(description='ltags: tag generator for Lean theorem prover.')
parser = argparse.ArgumentParser(description='leantags: tag generator for Lean theorem prover.')
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('--relative', action='store', default=None, const=os.getcwd(), nargs='?', help="Generate relative paths based on the parameter.")

22
bin/linja
View file

@ -45,7 +45,7 @@ g_lean_bin_dir = os.path.dirname(g_linja_path)
g_phony_targets = ["all", "clean", "tags", "clear-cache"]
g_project_filename = ".project"
g_lean_path = "USE DEFAULT" # System will search automatically
g_ltags_path = "USE DEFAULT" # System will search automatically
g_leantags_path = "USE DEFAULT" # System will search automatically
g_ninja_path = "USE DEFAULT" # System will search automatically
g_flycheck_header = "FLYCHECK_BEGIN"
g_flycheck_footer = "FLYCHECK_END"
@ -284,8 +284,8 @@ def find_location(exec_name):
return pathname
def check_requirements():
global g_lean_path, g_ltags_path, g_ninja_path
ltags_exec_name = "ltags"
global g_lean_path, g_leantags_path, g_ninja_path
leantags_exec_name = "leantags"
lean_exec_name = "lean"
ninja_exec_name = "ninja"
if platform.system() == "Windows" or platform.system().startswith("MSYS"):
@ -294,14 +294,14 @@ def check_requirements():
if g_lean_path == "USE DEFAULT":
g_lean_path = find_location(lean_exec_name)
if g_ltags_path == "USE DEFAULT":
g_ltags_path = find_location(ltags_exec_name)
if g_leantags_path == "USE DEFAULT":
g_leantags_path = find_location(leantags_exec_name)
if g_ninja_path == "USE DEFAULT":
g_ninja_path = find_location(ninja_exec_name)
if not os.path.isfile(g_lean_path):
error("cannot find lean executable at " + os.path.abspath(g_lean_path))
if not os.path.isfile(g_ltags_path):
error("cannot find ltags executable at " + os.path.abspath(g_ltags_path))
if not os.path.isfile(g_leantags_path):
error("cannot find leantags executable at " + os.path.abspath(g_leantags_path))
if not os.path.isfile(g_ninja_path):
g_ninja_path = download_ninja_and_save_at(g_ninja_path)
@ -378,7 +378,7 @@ def debug_status(args):
print "lean/bin dir =", g_lean_bin_dir
print "phony targets =", g_phony_targets
print "lean path =", g_lean_path
print "ltags path =", g_ltags_path
print "leantags path =", g_leantags_path
print "ninja path =", g_ninja_path
def handle_flycheck_failure(out, err, args):
@ -577,11 +577,11 @@ def make_build_ninja(args):
print >> f, """ command = "%s" %s "$in" -o "${OLEAN_FILE}" -c "${CLEAN_FILE}" -i "${ILEAN_FILE}" """ \
% (g_lean_path, " ".join(args.lean_options))
print >> f, """rule LTAGS"""
print >> f, """rule LEANTAGS"""
print >> f, """ command = """,
if platform.system() == "Windows":
print >> f, "python ",
print >> f, """"%s" --relative -- $in """ % (g_ltags_path)
print >> f, """"%s" --relative -- $in """ % (g_leantags_path)
print >> f, "build all: phony",
for item in lean_files:
@ -590,7 +590,7 @@ def make_build_ninja(args):
tags_file = "TAGS"
print >> f, "build tags: phony " + tags_file
print >> f, "build " + tags_file + ": LTAGS",
print >> f, "build " + tags_file + ": LEANTAGS",
for item in lean_files:
print >> f, " " + escape_ninja_char(item['ilean']),
print >> f, ""

2
src/CMakeLists.txt
View file

@ -397,7 +397,7 @@ add_custom_target(clean-hott-lib
add_custom_target(clean-olean
DEPENDS clean-std-lib clean-hott-lib)
install(FILES ${CMAKE_SOURCE_DIR}/../bin/linja ${CMAKE_SOURCE_DIR}/../bin/ltags
install(FILES ${CMAKE_SOURCE_DIR}/../bin/linja ${CMAKE_SOURCE_DIR}/../bin/leantags
DESTINATION bin
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE)

20
src/emacs/lean-tags.el
View file

@ -17,25 +17,25 @@
(defun lean-generate-tags ()
"Run linja TAGS and let emacs use the generated TAGS file."
(interactive)
(let* ((ltags-file-name (lean-get-executable "linja"))
ltags-command)
(setq ltags-command
(let* ((leantags-file-name (lean-get-executable "linja"))
leantags-command)
(setq leantags-command
(cond ((string= system-type "windows-nt")
(append '("python" nil "*lean-tags*" nil)
`(,ltags-file-name)
`(,leantags-file-name)
lean-flycheck-checker-options
'("tags")))
(t
(append `(,ltags-file-name nil "*lean-tags*" nil)
(append `(,leantags-file-name nil "*lean-tags*" nil)
lean-flycheck-checker-options
'("tags")))))
(message "Generating TAGS...")
(apply 'call-process ltags-command)
(apply 'call-process leantags-command)
(message "TAGS generated.")
(setq tags-table-list (lean-tags-table-list))))
(defmacro lean-tags-make-advice-to-call-ltags (f)
(defmacro lean-tags-make-advice-to-call-leantags (f)
(let* ((f-name (symbol-name f))
(advice-name (concat "lean-tags-advice-"
(symbol-name f))))
@ -45,7 +45,7 @@
(when (derived-mode-p 'lean-mode)
(lean-generate-tags)))))
(defvar-local functions-to-call-ltags-before-it
(defvar-local functions-to-call-leantags-before-it
'(find-tag-noselect
tags-search
tags-query-replace
@ -53,8 +53,8 @@
tags-apropos
select-tags-table))
(-each functions-to-call-ltags-before-it
(lambda (f) (eval `(lean-tags-make-advice-to-call-ltags ,f))))
(-each functions-to-call-leantags-before-it
(lambda (f) (eval `(lean-tags-make-advice-to-call-leantags ,f))))
(defun lean-find-tag ()
"lean-find-tag"