X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=pret-lam.lua;h=68db5772120fcf8716ada9e40b3f612a43986747;hp=1011b19e1672e24fb3cb572eaff45e4a4ffa17d5;hb=651af924b4870140446c9f3551b3aea1095d8987;hpb=9fb83d4c3f0511c8e6e0b584d18370eba508a29b diff --git a/pret-lam.lua b/pret-lam.lua index 1011b19..68db577 100644 --- a/pret-lam.lua +++ b/pret-lam.lua @@ -6,41 +6,50 @@ 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.symbols = { +-- Symbols that should have a different representation +local symbols = { [' '] = {repr = '\\obs '}, ['_'] = {repr = '\\_'}, ['->'] = {repr = '\\rightarrow'}, -- The default * sits very high above the baseline, \ast (u+2217) looks -- better. ['*'] = {repr = '\\ast'}, + ['~'] = {repr = '\\HDLine[width=.20 * \\the\\textwidth]'}, + ['|'] = {repr = '\\char' .. utf.byte('|')}, } -buffers.visualizers.lam.keywords = { +-- Keywords that should be bold +local keywords = { ['case'] = {}, ['of'] = {}, ['let'] = {}, + ['letrec'] = {}, + ['letnonrec'] = {}, ['in'] = {}, + ['DEFAULT'] = {}, } - -function buffers.visualizers.lam.take_symbol(str) - -- 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. - for symbol,props in pairs(buffers.visualizers.lam.symbols) do +local in_block = 0 +local submatches = {} +local bases = {} +-- Store the last line for each indent level +local indentlines = {} + +-- 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 symbol,props in pairs(symbols) do -- Try to remove symbol from the start of str symbol, newstr = utf.match(str, "^(" .. symbol .. ")(.*)") if symbol then @@ -60,15 +69,17 @@ end -- Take a single word from str, if posible. Returns the rest of the string and -- the word taken. -function buffers.visualizers.lam.take_word(str) - res, newstr = utf.match(str, "^(%a[%a%d_]+)(.*)") +local function take_word(str) + -- A word must always start with a-z (in particular, λ is not a valid + -- start of a word). + res, newstr = utf.match(str, "^([a-zA-Z][%a%d%+%-%,_]+)(.*)") 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. -function buffers.visualizers.lam.match_mul(str, patterns) +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 @@ -78,55 +89,136 @@ function buffers.visualizers.lam.match_mul(str, patterns) return nil end -function buffers.visualizers.lam.begin_of_buffer() - -- Initially allow subscripts using _ or just appending a number (later, - -- we will add extra patterns here. - submatches = {"^(.*)_([%a%d,]+)$", "^(.*[^%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 - -function buffers.visualizers.lam.end_of_buffer() - -- Reset submatches and bases, since flush_line can be called without - -- begin / end_of_buffer for \type. - buffers.visualizers.lam.begin_of_buffer() - bases = nil -end - -function buffers.visualizers.lam.do_subscripts(word) - local match_mul = buffers.visualizers.lam.match_mul +-- 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 bases and not bases[base] then + if not bases[base] then -- Register that we've added this base bases[base] = true - -- Add a pattern for this base - submatches[#submatches+1] = "^(" .. base .. ")([%a%d,]+)$" + -- 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 -function buffers.visualizers.lam.flush_line(str,nested) +-- 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,]+)$"} + -- 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) local result, state = { }, 0 local finish, change = buffers.finish_state, buffers.change_state - local take_symbol = buffers.visualizers.lam.take_symbol - local take_word = buffers.visualizers.lam.take_word - local do_subscripts = buffers.visualizers.lam.do_subscripts + str = do_indent(str) -- Set the colorscheme, which is used by finish_state and change_state - buffers.currentcolors = buffers.visualizers.lam.colors + buffers.currentcolors = colors while str ~= "" do local found = false local word, symbol -- See if the next token is a word word, str = take_word(str) if word then - if buffers.visualizers.lam.keywords[res] then + if keywords[res] then -- Make all keywords bold word = "{\\bold " .. word .. "}" else @@ -141,13 +233,9 @@ function buffers.visualizers.lam.flush_line(str,nested) -- Append the resulting token result[#result+1] = word or symbol end - + state = finish(state, result) buffers.flush_result(result,nested) end --- Call end_of_buffer once to set up submatches (since \type doesn't call --- begin_of_buffer / end_of_buffer). -buffers.visualizers.lam.end_of_buffer() - -- vim: set sw=4 sts=4 expandtab ai: