shared.py 1.99 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
from flask_sqlalchemy import SQLAlchemy

import re

import config

db = SQLAlchemy()

# the following code is written by Lars Beckers and not to be published without permission
latex_chars = [
    ("\\", "\\backslash"), # this needs to be first
    ("$", "\$"),
    ('%', '\\%'),
    ('&', '\\&'),
    ('#', '\\#'),
    ('_', '\\_'),
    ('{', '\\{'),
    ('}', '\\}'),
    #('[', '\\['),
    #(']', '\\]'),
    #('"', '"\''),
    ('~', '$\\sim{}$'),
    ('^', '\\textasciicircum{}'),
    ('Ë„', '\\textasciicircum{}'),
    ('`', '{}`'),
    ('-->', '$\longrightarrow$'),
    ('->', '$\rightarrow$'),
    ('==>', '$\Longrightarrow$'),
    ('=>', '$\Rightarrow$'),
    ('>=', '$\geq$'),
    ('=<', '$\leq$'),
    ('<', '$<$'),
    ('>', '$>$'),
    ('\\backslashin', '$\\in$'),
    ('\\backslash', '$\\backslash$') # this needs to be last
]

def escape_tex(text):
    out = text
    for old, new in latex_chars:
        out = out.replace(old, new)
    # beware, the following is carefully crafted code
    res = ''
    k, l = (0, -1)
    while k >= 0:
        k = out.find('"', l+1)
        if k >= 0:
            res += out[l+1:k]
            l = out.find('"', k+1)
            if l >= 0:
                res += '\\enquote{' + out[k+1:l] + '}'
            else:
                res += '"\'' + out[k+1:]
            k = l
        else:
            res += out[l+1:]
    # yes, this is not quite escaping latex chars, but anyway...
    res = re.sub('([a-z])\(', '\\1 (', res)
    res = re.sub('\)([a-z])', ') \\1', res)
    #logging.debug('escape latex ({0}/{1}): {2} --> {3}'.format(len(text), len(res), text.split('\n')[0], res.split('\n')[0]))
    return res

def unhyphen(text):
    return " ".join([r"\mbox{" + word + "}" for word in text.split(" ")])

def date_filter(date):
    return date.strftime("%d. %B %Y")
def datetime_filter(date):
    return date.strftime("%d. %B %Y, %H:%M")
def date_filter_long(date):
    return date.strftime("%A, %d.%m.%Y, Kalenderwoche %W")
def time_filter(time):
    return time.strftime("%H:%m")