X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=pret-lam.lua;h=feaa5e43934cbb157757b9152c38a6ea8f624c72;hp=f8ddb676088a7870fd94a979276d3283aa7b7dd6;hb=0dfecb0be783911fd804436c22bbbf8c79711cc3;hpb=754983b9ff12abf4fd16b7f7a2d2bf7e0b024f0c diff --git a/pret-lam.lua b/pret-lam.lua index f8ddb67..feaa5e4 100644 --- a/pret-lam.lua +++ b/pret-lam.lua @@ -19,17 +19,20 @@ local colors = { local symbols = { -- Note, the space we replace with is a Unicode non-breaking space -- (U+00A0). - [' '] = {repr = ' '}, - ['_'] = {repr = '\\_'}, - ['->'] = {repr = '→'}, - ['=>'] = {repr = '⇒'}, + {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'}, - ['~'] = {repr = '\\HDLine[width=.20 * \\the\\textwidth]'}, - ['|'] = {repr = '\\char' .. utf.byte('|')}, - -- Use ▶ from our roman font, since Iwona doesn't have the glyph - ['▶'] = {repr = '{\\rm{}▶}'}, + {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{}∧}'}, } -- Keywords that should be bold @@ -63,9 +66,9 @@ end -- 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 + for i,props in ipairs(symbols) do -- Try to remove symbol from the start of str - symbol, newstr = utf.match(str, "^(" .. symbol .. ")(.*)") + symbol, newstr = utf.match(str, "^(" .. props.symbol .. ")(.*)") if symbol then -- Return this tokens repr, or just the token if it has no -- repr. @@ -85,8 +88,12 @@ end -- 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). - res, newstr = utf.match(str, "^([a-zA-Z][%a%d%+%-%,_]+)(.*)") + -- 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 @@ -206,7 +213,7 @@ 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,]+)$"} + 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. @@ -221,12 +228,16 @@ 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), nested) + buffers.flush_result(vis.do_line(str, false), nested) end -function vis.do_line(str) - result = {} - str = do_indent(str) +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 local found = false local word, symbol @@ -234,10 +245,17 @@ function vis.do_line(str) if text then table.insert(result, '\\strikethrough{') -- Recursively call ourselves to handle spaces gracefully. - result = array_concat(result, vis.do_line(text)) + 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)