From 37a11d25bdf895354b1c0e8c693f19205a2884a7 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 27 Apr 2011 10:08:43 +0000
Subject: [PATCH] Parser accepts unicode (e.g. in comments).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2830 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/PrismParser.java             | 48 +++++++++----------
 prism/src/parser/PrismParser.jj               |  1 +
 prism/src/parser/PrismParserTokenManager.java | 22 ++++++++-
 3 files changed, 45 insertions(+), 26 deletions(-)

diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java
index d51858e0..f0ce22ca 100644
--- a/prism/src/parser/PrismParser.java
+++ b/prism/src/parser/PrismParser.java
@@ -3033,30 +3033,6 @@ public class PrismParser implements PrismParserConstants {
     finally { jj_save(12, xla); }
   }
 
-  static private boolean jj_3R_68() {
-    if (jj_scan_token(OR)) return true;
-    if (jj_3R_67()) return true;
-    return false;
-  }
-
-  static private boolean jj_3R_116() {
-    Token xsp;
-    xsp = jj_scanpos;
-    if (jj_3R_139()) {
-    jj_scanpos = xsp;
-    if (jj_3R_140()) {
-    jj_scanpos = xsp;
-    if (jj_3R_141()) return true;
-    }
-    }
-    if (jj_scan_token(LBRACKET)) return true;
-    if (jj_3R_142()) return true;
-    xsp = jj_scanpos;
-    if (jj_3R_143()) jj_scanpos = xsp;
-    if (jj_scan_token(RBRACKET)) return true;
-    return false;
-  }
-
   static private boolean jj_3_12() {
     if (jj_3R_29()) return true;
     if (jj_scan_token(LPARENTH)) return true;
@@ -4259,6 +4235,30 @@ public class PrismParser implements PrismParserConstants {
     return false;
   }
 
+  static private boolean jj_3R_68() {
+    if (jj_scan_token(OR)) return true;
+    if (jj_3R_67()) return true;
+    return false;
+  }
+
+  static private boolean jj_3R_116() {
+    Token xsp;
+    xsp = jj_scanpos;
+    if (jj_3R_139()) {
+    jj_scanpos = xsp;
+    if (jj_3R_140()) {
+    jj_scanpos = xsp;
+    if (jj_3R_141()) return true;
+    }
+    }
+    if (jj_scan_token(LBRACKET)) return true;
+    if (jj_3R_142()) return true;
+    xsp = jj_scanpos;
+    if (jj_3R_143()) jj_scanpos = xsp;
+    if (jj_scan_token(RBRACKET)) return true;
+    return false;
+  }
+
   static private boolean jj_initialized_once = false;
   /** Generated Token Manager. */
   static public PrismParserTokenManager token_source;
diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj
index bd9d51e1..c41a0488 100644
--- a/prism/src/parser/PrismParser.jj
+++ b/prism/src/parser/PrismParser.jj
@@ -26,6 +26,7 @@
 
 options {
 	LOOKAHEAD = 1;
+	UNICODE_INPUT = true;
 }
 
 PARSER_BEGIN(PrismParser)
diff --git a/prism/src/parser/PrismParserTokenManager.java b/prism/src/parser/PrismParserTokenManager.java
index 1c4638da..de290989 100644
--- a/prism/src/parser/PrismParserTokenManager.java
+++ b/prism/src/parser/PrismParserTokenManager.java
@@ -827,6 +827,9 @@ static private int jjStartNfaWithStates_0(int pos, int kind, int state)
    return jjMoveNfa_0(state, pos + 1);
 }
 static final long[] jjbitVec0 = {
+   0xfffffffffffffffeL, 0xffffffffffffffffL, 0xffffffffffffffffL, 0xffffffffffffffffL
+};
+static final long[] jjbitVec2 = {
    0x0L, 0x0L, 0xffffffffffffffffL, 0xffffffffffffffffL
 };
 static private int jjMoveNfa_0(int startState, int curPos)
@@ -1045,6 +1048,9 @@ static private int jjMoveNfa_0(int startState, int curPos)
       }
       else
       {
+         int hiByte = (int)(curChar >> 8);
+         int i1 = hiByte >> 6;
+         long l1 = 1L << (hiByte & 077);
          int i2 = (curChar & 0xff) >> 6;
          long l2 = 1L << (curChar & 077);
          do
@@ -1052,11 +1058,11 @@ static private int jjMoveNfa_0(int startState, int curPos)
             switch(jjstateSet[--i])
             {
                case 2:
-                  if ((jjbitVec0[i2] & l2) != 0L)
+                  if (jjCanMove_0(hiByte, i1, i2, l1, l2))
                      jjAddStates(4, 6);
                   break;
                case 16:
-                  if ((jjbitVec0[i2] & l2) != 0L)
+                  if (jjCanMove_0(hiByte, i1, i2, l1, l2))
                      jjAddStates(12, 13);
                   break;
                default : break;
@@ -1079,6 +1085,18 @@ static private int jjMoveNfa_0(int startState, int curPos)
 static final int[] jjnextStates = {
    10, 11, 12, 18, 2, 3, 5, 20, 21, 22, 13, 14, 16, 17, 
 };
+private static final boolean jjCanMove_0(int hiByte, int i1, int i2, long l1, long l2)
+{
+   switch(hiByte)
+   {
+      case 0:
+         return ((jjbitVec2[i2] & l2) != 0L);
+      default :
+         if ((jjbitVec0[i1] & l1) != 0L)
+            return true;
+         return false;
+   }
+}
 
 /** Token literal values. */
 public static final String[] jjstrLiteralImages = {