export decl name database

[robertylewis]

This creates a file export_db.json mapping declaration names to information about them. Specifically:

• 'filename': the local absolute path to the file containing this decl. This can be used to identify if a declaration is in core or not. I'm not sure if it's really needed, maybe it should be replaced with an is_core flag?
• line: the line number of the decl in source
• args: arguments to the declaration that appear "left of the colon." Effectively, anything with dependencies to the right.
• type: the type of the declaration "right of the colon." See note below.
• src_link: link to the decl's location on GitHub
• docs_link: link to the decl's location in the docs

Note 1: due to a discrepancy in how we collect info about structure fields/constructors, these will never have entries in args. Their type will be written out fully in type.

Note 2: the type information is still decorated to associate notation to its corresponding declaration. The doc generation uses this function to undecorate and linkify:

def linkify_linked(string, loc_map):
  return ''.join(
    match[4] if match[0] == '' else
    match[1] + linkify_core(match[0], match[2], loc_map) + match[3]
    for match in re.findall(r'\ue000(.+?)\ue001(\s*)(.*?)(\s*)\ue002|([^\ue000]+)', string))

There's enough information in this map to reimplement the linkification if desired. Otherwise, the \ue00* decorations should be stripped before displaying.

\cc @PatrickMassot

[gebner]

The decoration markup syntax used in type is described in this PR: leanprover-community/lean#89

This PR adds the option pp.links which, if set to true, annotates things like ℤ and + and the fst in p.fst with the corresponding constant names (i.e., int, has_add.add, and prod.fst). The markup syntax for this annotation is as follows:

<U+E000>prod.fst<U+E001>fst<U+E002>

The Unicode code points U+E000, U+E001, U+E002 are taken from the Private Use Area. Hopefully nobody uses them for anything else.

[robertylewis]

I'm going to merge this; @bryangingechen if you see anything you'd like to change, feel free to push or PR!