From e03012cc77fd8c0b82e618cdd19301259bcbb8b1 Mon Sep 17 00:00:00 2001
From: Katja Goltsova <katja.goltsova@protonmail.com>
Date: Tue, 4 Oct 2022 14:51:45 +0200
Subject: [PATCH] Allow more characters in identifiers
---
lisa-utils/src/main/scala/lisa/utils/Parser.scala | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/lisa-utils/src/main/scala/lisa/utils/Parser.scala b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
index 7b6eda22..279590a9 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Parser.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Parser.scala
@@ -153,6 +153,7 @@ object Parser {
// TODO: add positions ==> ranges to tokens
type Position = Unit
+ private val allowedIdentifierCharacters = elem(_.isLetter) | elem(_.isDigit) | oneOf("_\\@#$%^&*><:|_+-=")
private val schematicSymbol = "'"
private val lexer = Lexer(
@@ -174,11 +175,11 @@ object Parser {
elem(';') |> SemicolonToken,
elem('⊢') | word("|-") |> SequentToken,
many1(whiteSpace) |> SpaceToken,
- word(schematicSymbol) ~ many1(elem(_.isLetter) | elem('_') | elem(_.isDigit) | elem('\'')) |> { cs =>
+ word(schematicSymbol) ~ many1(allowedIdentifierCharacters) |> { cs =>
// drop the '
SchematicToken(cs.drop(1).mkString)
},
- many1(elem(_.isLetter) | elem('_') | elem(_.isDigit)) |> { cs => ConstantToken(cs.mkString) }
+ many1(allowedIdentifierCharacters) |> { cs => ConstantToken(cs.mkString) }
) onError { (cs, _) =>
throw ParserException(s"Unexpected input: ${cs.mkString}")
}
--
GitLab