X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=pret-lam.lua;h=feaa5e43934cbb157757b9152c38a6ea8f624c72;hp=7bb1f8a6cab40d376b1269db23381f39b8aa0f46;hb=1993a03662ae0fb9a0ca57d8faf5f7f810fff749;hpb=f4487c5200e90a7b0d9db0319324335fd55e810b diff --git a/pret-lam.lua b/pret-lam.lua index 7bb1f8a..feaa5e4 100644 --- a/pret-lam.lua +++ b/pret-lam.lua @@ -6,62 +6,280 @@ local utf = unicode.utf8 -if not buffers then buffers = { } end -if not buffers.visualizers then buffers.visualizers = { } end -if not buffers.visualizers.lam then buffers.visualizers.lam = { } end +local vis = buffers.newvisualizer("lam") -buffers.visualizers.lam.colors = { +local colors = { "prettytwo", "prettyone", "prettythree", "prettyfour" } -buffers.visualizers.lam.tokens = { - [' '] = {repr = '\\obs '}, - ['_'] = {repr = '\\_'}, - ['->'] = {repr = '\\rightarrow'}, +-- Symbols that should have a different representation +local symbols = { + -- Note, the space we replace with is a Unicode non-breaking space + -- (U+00A0). + {symbol = ' ', repr = ' '}, + {symbol = '_', repr = '\\_'}, + {symbol = '->>', repr = '\\twoheadrightarrow'}, + {symbol = '->', repr = '→'}, + {symbol = '=>', repr = '⇒'}, -- The default * sits very high above the baseline, \ast (u+2217) looks -- better. - ['*'] = {repr = '\\ast'}, - ['case'] = {style = 'bold'}, - ['of'] = {style = 'bold'}, - ['let'] = {style = 'bold'}, - ['in'] = {style = 'bold'}, + {symbol = '*', repr = '\\ast'}, + {symbol = '~', repr = '\\HDLine[width=.20 * \\the\\textwidth]'}, + {symbol = '|', repr = '\\char' .. utf.byte('|')}, + -- Use ▶ and ∧ from our roman font, since Iwona doesn't have the glyph + {symbol = '▶', repr = '{\\rm{}▶}'}, + --{symbol = '∧', repr = '{$∧$}'}, + {symbol = '∧', repr = '{\\rm{}∧}'}, } -function buffers.visualizers.lam.flush_line(str,nested) - local result, state = { }, 0 - local finish, change = buffers.finish_state, buffers.change_state - -- Set the colorscheme, which is used by finish_state and change_state - buffers.currentcolors = buffers.visualizers.lam.colors +-- Keywords that should be bold +local keywords = { + ['case'] = {}, + ['of'] = {}, + ['let'] = {}, + ['letrec'] = {}, + ['letnonrec'] = {}, + ['in'] = {}, + ['DEFAULT'] = {small = true}, +} + +local in_block = 0 +local submatches = {} +local bases = {} +-- Store the last line for each indent level +local indentlines = {} + +function array_concat(a1, a2) + local res = a1 + for k,v in ipairs(a2) do + table.insert(res, v) + end + return res +end + + +-- See if str starts with a symbol, and return the remaining string and that +-- symbol. If no symbol from the table is matched, just returns the first +-- character. We can do a lookup directly, since symbols can be different in +-- length, so we just loop over all symbols, trying them in turn. +local function take_symbol(str) + for i,props in ipairs(symbols) do + -- Try to remove symbol from the start of str + symbol, newstr = utf.match(str, "^(" .. props.symbol .. ")(.*)") + if symbol then + -- Return this tokens repr, or just the token if it has no + -- repr. + res = props.repr or symbol + -- Enclose the token in {\style .. } + if props.style then + res = "{\\" .. props.style .. " " .. res .. "}" + end + return res, newstr + end + end + -- No symbol found, just return the first character + return utf.match(str, "^(.)(.*)") +end + +-- Take a single word from str, if posible. Returns the rest of the string and +-- the word taken. +local function take_word(str) + -- A word must always start with a-z (in particular, λ is not a valid + -- start of a word). A word must always end with a letter or a digit + res, newstr = utf.match(str, "^([a-zA-Z][%a%d%+%-%,_]*[%a%d]+)(.*)") + if not res then + -- The above does not catch single letter words + res, newstr = utf.match(str, "^([a-zA-Z])(.*)") + end + return res, newstr or str +end + +-- Tries to match each of the patterns and returns the captures of the first +-- matching pattern (up to 5 captures are supported). Returns nil when nothing +-- matches. +local function match_mul(str, patterns) + for i, pat in ipairs(patterns) do + a, b, c, d, e = utf.match(str, pat) + if a then + return a, b, c, d, e + end + end + return nil +end + +-- Find any subscripts in the given word and typeset them +local function do_subscripts(word) + base, sub = match_mul(res, submatches) + if sub then + word = base .. "\\low{" .. sub .. "}" + -- After a word has been used as a base, allow subscripts + -- without _, even for non-numbers. + if not bases[base] then + -- Register that we've added this base + bases[base] = true + -- Add a patterns for this base. First, the base with a single + -- letter or number subscript. + submatches[#submatches+1] = "^(" .. base .. ")([%a%d])$" + -- Seconde, the base with a longer prefix that includes at least + -- one of +-, (to catch things like ri+1, but not return). + submatches[#submatches+1] = "^(" .. base .. ")([%a%d]*[%-%+,]+[%a%d%-%+,]*)$" + end + end + return word +end + +-- Do proper aligning for subsequent lines. For example, in +-- foo = bar +-- | baz +-- We replace the spaces in the second line with a skip with the same with as +-- "foo ", to align the | with the =. +-- For this, we keep a table "indentlines", which contains all previous lines +-- with smaller indent levels that are still "in scope" (e.g., have not yet +-- been followed by a line with a smaller indent level). For example: +-- line1 +-- line2 +-- line3 +-- line4 +-- line5 +-- After the last line, the table will contain: +-- { 0 = "line1", 2 = " line4", 4 = " line5"} +-- In other words, line3 is no longer in scope since it is "hidden" by +-- line4, and line is no longer in scope since it is replaced by line4. +local function do_indent(line) + newind, rest = utf.match(line, '^(%s*)(.*)') + prev = -1 + -- Loop all the previous lines + for indent, unused in pairs(indentlines) do + if indent > #newind then + -- Remove any lines with a larger indent + indentlines[indent] = nil + elseif indent < #newind and indent > prev then + -- Find the last line (e.g, with the highest indent) with an + -- indent smaller than the new indent. This is the line from which + -- we need to copy the indent. + prev = indent + end + end + + -- Always store this line, possibly overwriting a previous line with the + -- same indent + indentlines[#newind] = line + if prev ~= -1 then + -- If there is a previous line with a smaller indent, make sure we + -- align with it. We do this by taking a prefix from that previous + -- line just as long as our indent. This gives us a bunch of + -- whitespace, with a few non-whitespace characters. We find out the + -- width of this prefix, and put whitespace just as wide as that + -- prefix before the current line, instead of the whitespace + -- characters that were there. + -- Doing this is slightly risky, since the prefix might contain + -- unfinished markup (e.g., \foo{bar without the closing }). We might + -- need to solve this later. + copyind = utf.sub(indentlines[prev], 1, #newind) + setwidth = "\\setwidthof{" .. copyind .. "}\\to\\pretlamalignwidth" + hskip = "\\hskip\\pretlamalignwidth" + return "{" .. setwidth .. hskip .. "}" .. rest + end + -- No previous line? Just return the unmodified line then + return line +end + + +-- Mark the begin of a block of lambda formatted buffers or expressions. This +-- means that, until you call end_of_block again, the subscript bases are +-- shared. For example, if you have \lam{y1} some text \lam{yn} within a +-- single block, the yn will properly get subscripted. Be sure to call +-- end_of_block again! +-- +-- Blocks can be partially nested, meaning that the block +-- won't be closed until end_of_block was called exactly as often as +-- begin_of_block. However, subscripts from the inner block can still +-- influence subscripts in the outer block. +function vis.begin_of_block() + vis.begin_of_display() + in_block = in_block + 1 +end + +-- Ends the current block +function vis.end_of_block() + in_block = in_block - 1 +end + +function vis.begin_of_display() + if in_block == 0 then + -- Initially allow subscripts using _ or just appending a number (later, + -- we will add extra patterns here. + submatches = {"^(%a*)_([%a%d,]+)$", "^(%a+)(%d[%d,]*)$"} + -- This stores all the bases we've encountered so far (to prevent + -- duplicates). For each of them there will be a pattern in submatches + -- above. + bases = {} + end + indentlines = {} +end + + +-- Make things work for inline typeing (e.g., \type{}) as well. +vis.begin_of_inline = vis.begin_of_display +vis.end_of_inline = vis.end_of_display + +function vis.flush_line(str,nested) + buffers.flush_result(vis.do_line(str, false), nested) +end + +function vis.do_line(str, no_indent) + local result = {} + if not no_indent then + -- Allow ignore of the indentation stuff when we're calling ourselves + -- for a partial line. + str = do_indent(str) + end while str ~= "" do - found = false - for tok,props in pairs(buffers.visualizers.lam.tokens) do - -- Try to remove tok from the start of str - str, count = utf.gsub(str, "^" .. tok, "") - if count ~= 0 then - -- Replace the token with the repr, or just itself - result[#result+1] = props.repr or tok - -- Enclose the token in {\style .. } - if props.style then - result[#result] = "{\\" .. props.style .. - " " .. result[#result] .. - "}" + local found = false + local word, symbol + local text, rest = utf.match(str, "^%-%-(.-)%-%-(.*)") + if text then + table.insert(result, '\\strikethrough{') + -- Recursively call ourselves to handle spaces gracefully. + result = array_concat(result, vis.do_line(text, true)) + table.insert(result, '}') + -- Eat the processed characters + str = rest + elseif utf.match(str, "^%-%-") then + table.insert(result, '{\\italic{--') + -- Recursively call ourselves to handle spaces gracefully. + result = array_concat(result, vis.do_line(utf.sub(str, 3), true)) + table.insert(result, '}}') + -- Done with this line + str = '' + else + -- See if the next token is a word + word, str = take_word(str) + if word then + if keywords[res] then + -- Make all keywords bold + word = "{\\bold " .. word .. "}" + if keywords[res].small then + word = "\\small" .. word -- Curlies were added above + end + else + -- Process any subscripts in the word + word = do_subscripts(word) end - -- We found a token, now start over - found = true - break + table.insert(result, word) + else + -- The next token is not a word, it must be a symbol + symbol, str = take_symbol(str) + table.insert(result, symbol) end end - if not found then - result[#result+1] = utf.sub(str, 1, 1) - str = utf.sub(str, 2) - end end - state = finish(state, result) - buffers.flush_result(result,nested) + + return result end -- vim: set sw=4 sts=4 expandtab ai: