From f928b2bae39a65f50c29b27f75f54a7115814ccc Mon Sep 17 00:00:00 2001
From: Moritz Dieing <63721811+moritzdieing@users.noreply.github.com>
Date: Fri, 2 Jul 2021 14:47:25 +0200
Subject: [PATCH] Optimise type assumption syntax
---
frontend/src/type-input-listener.ts | 4 ++--
src/main/resources/language/general.properties | 3 ++-
2 files changed, 4 insertions(+), 3 deletions(-)
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