isa-parser: recordUpd: fieldL instead of termL for field name

au-ts · Jan 15, 2020 · a2085cd · a2085cd
1 parent cd081fe
commit a2085cd
Showing 1 changed file with 10 additions and 2 deletions.
diff --git a/isa-parser/Isabelle/Parser.hs b/isa-parser/Isabelle/Parser.hs
@@ -615,10 +615,18 @@ recordUpdTermL = do { stringL "\\<lparr>"
                     ; return $ RecordUpd upds }
 
 updTermL :: ParserM (Term, Term)
-updTermL = do { term1 <- termL
+updTermL = do { term1 <- fieldL
               ; stringL ":="
               ; term2 <- termL
-              ; return (term1, term2) }
+              ; return (AntiTerm term1, term2) }
+
+fieldL :: ParserM String 
+fieldL = notReservedLexeme fieldS 
+
+fieldS :: ParserM String 
+fieldS = letterS <++> manyP fieldLetters
+    where 
+      fieldLetters = ((letterS <||> digitS <||> charString '_') <||> charString '\'' <||> charString '.') <?> "quasi-letter"
 
 caseOfTermL :: ParserM Term
 caseOfTermL = do { stringL "case"