X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=pret-lam.lua;h=a87137c0dc0b2428a1484552fe7d0357781f2fcf;hp=c25daefb697c3cd08c7a15115c935a62a948cf42;hb=6493f3173bbe36cdcd51ea6fc607966e10373944;hpb=72702b3b4183aa6cf75fe01ae5a07aaf85790801 diff --git a/pret-lam.lua b/pret-lam.lua index c25daef..a87137c 100644 --- a/pret-lam.lua +++ b/pret-lam.lua @@ -21,6 +21,9 @@ buffers.visualizers.lam.tokens = { [' '] = {repr = '\\obs '}, ['_'] = {repr = '\\_'}, ['->'] = {repr = '\\rightarrow'}, + -- The default * sits very high above the baseline, \ast (u+2217) looks + -- better. + ['*'] = {repr = '\\ast'}, ['case'] = {style = 'bold'}, ['of'] = {style = 'bold'}, ['let'] = {style = 'bold'}, @@ -53,8 +56,10 @@ function buffers.visualizers.lam.flush_line(str,nested) end end if not found then - result[#result+1] = utf.sub(str, 1, 1) - str = utf.sub(str, 2) + -- Take a full word, or a single character. Taking a full word is + -- to prevent matching "in" in "bind" , for example. + result[#result+1] = utf.match(str, "^%a+") or utf.sub(str, 1, 1) + str = utf.sub(str, utf.len(result[#result]) + 1) end end state = finish(state, result)