#!/usr/bin/env lua5.1
-- This file:
--   http://anggtwu.net/LUA/LeanMetaDoc1.lua.html
--   http://anggtwu.net/LUA/LeanMetaDoc1.lua
--          (find-angg "LUA/LeanMetaDoc1.lua")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- Process the source files of 
--      (find-es "lean" "metaprogramming")
-- Generate lines like these:
--   (find-leanmetadoc  "main/05_syntax#declaring-syntax")
--   (find-leanmetadocr "main/05_syntax" "## Declaring Syntax")
--   (find-leanmetadoc  "main/05_syntax#declaration-helpers")
--   (find-leanmetadocr "main/05_syntax" "### Declaration helpers")
-- See: (find-angg "LEAN/syntax.lean")
--
-- (defun e () (interactive) (find-angg "LUA/LeanMetaDoc1.lua"))
--
-- «.getopt»		(to "getopt")
-- «.process-sections»	(to "process-sections")

mklinks0 = function (li, tag0)
    local fmt = '-- (find-leanmetadoc  "'..stem..'#%s")\n'
             .. '-- (find-leanmetadocr "'..stem..'" "%s")'
    return format(fmt, tag0, li)
  end
mklinks = function (li)
    local tag = li:match"^##+ (.*)$"
    tag = string.lower(tag)
    tag = tag:gsub("['`()?:;,./<>\"]", "")
    tag = tag:gsub(" ", "-")
    return mklinks0(li, tag)
  end

process = function (stem0)
    stem  = stem0 or "main/05_syntax"
    fname = format("~/usrc/lean4-metaprogramming-book/lean/%s.lean", stem)
    bigstr = ee_readfile(fname)
    fmt0 = '-- (find-sh "~/LUA/LeanMetaDoc1.lua -stem %s")\n'
    fmt1 = '-- (find-angg "LUA/LeanMetaDoc1.lua" "process-sections")\n'
    fmt2 = '-- (find-leanmetadoc  "%s")\n'
    fmt3 = '-- (find-leanmetadocr "%s")\n'
    printf(fmt0, stem)
    printf(fmt1, stem)
    printf(fmt2, stem)
    printf(fmt3, stem)
    for _,li in ipairs(splitlines(bigstr)) do
      local body = li:match"^(##+ .*)$"
                or li:match"^/%- (##+ .*) %-/$"
      if body then
        print(mklinks(body))
      end
    end
  end

-- «getopt»  (to ".getopt")
-- Test: (find-sh "~/LUA/LeanMetaDoc1.lua -stem main/01_intro")
--
Path.addLUAtopath()
require   "GetOpt1"    -- (find-angg "LUA/GetOpt1.lua")
mygetopt = GetOpt {
  ["-stem"] = function (g,s) process(stem) g:rest(2) end,
}
mygetopt:run(unpack(arg or {}))


-- «process-sections»  (to ".process-sections")
--[[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "LeanMetaDoc1.lua"
process()

process("main/01_intro")
process("main/02_overview")
process("main/03_expressions")
process("main/04_metam")
process("main/05_syntax")
process("main/06_macros")
process("main/07_elaboration")
process("main/08_dsls")
process("main/09_tactics")
process("main/10_cheat-sheet")
process("extra/01_options")
process("extra/02_attributes")
process("extra/03_pretty-printing")
process("solutions/03_expressions")
process("solutions/04_metam")
process("solutions/05_syntax")
process("solutions/07_elaboration")
process("solutions/09_tactics")

--]]





-- Local Variables:
-- coding:  utf-8-unix
-- End: