diff --git a/frontend/src/type-input-listener.ts b/frontend/src/type-input-listener.ts index 13001ec..b83b083 100644 --- a/frontend/src/type-input-listener.ts +++ b/frontend/src/type-input-listener.ts @@ -19,8 +19,8 @@ function modifyValue(area: HTMLInputElement) { const value = parseBack(area.value); const start = area.selectionStart; const end = area.selectionEnd; - // ignore brackets, allow '>', spaces, ':', '.' or '∀' in front and '-', spaces, '.', ':' or ';' at the end of string - area.value = value.replace(/(^|\s+|\(|\)|>|∀|:|\.)t[0-9]+(?=\s+|\)|\(|-|:|\.|;|$)/ig, replacer); + // ignore brackets, allow '>', spaces, ':', '.', ',' or '∀' in front and '-', spaces, '.', ':', ',' or ';' at the end of string + area.value = value.replace(/(^|\s+|\(|\)|>|∀|:|,|\.)t[0-9]+(?=\s+|\)|\(|-|:|\.|;|,|$)/ig, replacer); area.selectionStart = start; area.selectionEnd = end; } diff --git a/src/main/resources/language/general.properties b/src/main/resources/language/general.properties index 35cfc6b..c829e3c 100644 --- a/src/main/resources/language/general.properties +++ b/src/main/resources/language/general.properties @@ -23,10 +23,11 @@ root.termGrammar=\u2329Term\u232A ::= (\u2329Term\u232A) | \u2329App\u232A | \u2 \u2329Const\u232A ::= [0-9]+ | true | false root.typeGrammar=\u2329Type\u232A ::= \u2329QuantifiedType\u232A | \u2329NormalType\u232A
\ -\u2329QuantifiedType\u232A ::= \u2329VarType\u232A.\u2329NormalType\u232A
\ +\u2329QuantifiedType\u232A ::= \u2329EnumVarType\u232A.\u2329NormalType\u232A
\ \u2329NormalType\u232A ::= (\u2329NormalType\u232A) | \u2329NamedType\u232A | \u2329VarType\u232A | \ \u2329FunctionType\u232A
\ \u2329NamedType\u232A ::= [a-zA-Z][a-zA-Z0-9]*  \\t[0-9]+
\ +\u2329EnumVarType\u232A ::= \u2329VarType\u232A , \u2329EnumVarType\u232A | \u2329VarType\u232A
\ \u2329VarType\u232A ::= t[0-9]+
\ \u2329FunctionType\u232A ::= \u2329NormalType\u232A -> \u2329NormalType\u232A