Merge pull request #1 from adelon/main

Update Fork

7 files changed, 67 insertions, 64 deletions

diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index 7a9a42d..1d13693 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -27,7 +27,7 @@ import Base hiding (many)
 
 import Control.Monad.Combinators
 import Control.Monad.State.Strict
-import Data.Char (isAsciiLower)
+import Data.Char (isAsciiLower, isDigit)
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Text qualified as Text
 import Prettyprinter (Pretty(..))
@@ -392,7 +392,10 @@ ref = lexeme do
         _ -> Char.char '}' *> pure (Ref ms)
 
 marker :: Lexer Text
-marker = takeWhile1P Nothing (\x -> isAsciiLower x || x == '_')
+marker = do
+    c <- satisfy isAsciiLower
+    cs <- takeWhileP Nothing (\x -> isAsciiLower x || isDigit x || x == '_')
+    pure (Text.cons c cs)
 
 -- | Parses the end of an environment.
 -- Commits only after having seen "\end{".
diff --git a/test/examples/byRef.tex b/test/examples/byRef.tex
index c896c86..8fd1e71 100644
--- a/test/examples/byRef.tex
+++ b/test/examples/byRef.tex
@@ -1,25 +1,25 @@
-\begin{proposition}\label{first_proposition}
+\begin{proposition}\label{prop1}
     $a = a$.
 \end{proposition}
 
-\begin{proposition}\label{second_proposition}
+\begin{proposition}\label{prop2}
     $b = b$.
 \end{proposition}
 
-\begin{proposition}\label{third_proposition}
+\begin{proposition}\label{prop3}
     $c = c$.
 \end{proposition}
 \begin{proof}
-    Follows by \ref{first_proposition}. % Should filter out second_proposition
+    Follows by \ref{prop1}. % Should filter out second_proposition
 \end{proof}
 
-\begin{proposition}\label{fourth_proposition}
+\begin{proposition}\label{prop4}
     $e = e$.
 \end{proposition}
 \begin{proof}
-    For all $d$ we have $d = d$ by \ref{first_proposition}.
+    For all $d$ we have $d = d$ by \ref{prop1}.
 \end{proof}
 
-\begin{proposition}\label{fifth_proposition}
+\begin{proposition}\label{prop5}
     $f = f$.
 \end{proposition}
diff --git a/test/golden/byRef/encoding tasks.golden b/test/golden/byRef/encoding tasks.golden
index 75c9e78..47513ec 100644
--- a/test/golden/byRef/encoding tasks.golden
+++ b/test/golden/byRef/encoding tasks.golden
@@ -1,22 +1,22 @@
-fof(first_proposition,conjecture,fa=fa).
+fof(prop1,conjecture,fa=fa).
 ------------------
-fof(second_proposition,conjecture,fb=fb).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
+fof(prop2,conjecture,fb=fb).
+fof(prop1,axiom,![Xa]:Xa=Xa).
 ------------------
-fof(third_proposition,conjecture,fc=fc).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
+fof(prop3,conjecture,fc=fc).
+fof(prop1,axiom,![Xa]:Xa=Xa).
 ------------------
-fof(fourth_proposition,conjecture,![Xd]:Xd=Xd).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
+fof(prop4,conjecture,![Xd]:Xd=Xd).
+fof(prop1,axiom,![Xa]:Xa=Xa).
 ------------------
-fof(fourth_proposition,conjecture,fe=fe).
-fof(third_proposition,axiom,![Xc]:Xc=Xc).
-fof(second_proposition,axiom,![Xb]:Xb=Xb).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
-fof(fourth_proposition1,axiom,![Xd]:Xd=Xd).
+fof(prop4,conjecture,fe=fe).
+fof(prop3,axiom,![Xc]:Xc=Xc).
+fof(prop2,axiom,![Xb]:Xb=Xb).
+fof(prop1,axiom,![Xa]:Xa=Xa).
+fof(prop41,axiom,![Xd]:Xd=Xd).
 ------------------
-fof(fifth_proposition,conjecture,ff=ff).
-fof(fourth_proposition,axiom,![Xe]:Xe=Xe).
-fof(third_proposition,axiom,![Xc]:Xc=Xc).
-fof(second_proposition,axiom,![Xb]:Xb=Xb).
-fof(first_proposition,axiom,![Xa]:Xa=Xa).
\ No newline at end of file
+fof(prop5,conjecture,ff=ff).
+fof(prop4,axiom,![Xe]:Xe=Xe).
+fof(prop3,axiom,![Xc]:Xc=Xc).
+fof(prop2,axiom,![Xb]:Xb=Xb).
+fof(prop1,axiom,![Xa]:Xa=Xa).
\ No newline at end of file
diff --git a/test/golden/byRef/generating tasks.golden b/test/golden/byRef/generating tasks.golden
index 3187198..b9fa157 100644
--- a/test/golden/byRef/generating tasks.golden
+++ b/test/golden/byRef/generating tasks.golden
@@ -1,7 +1,7 @@
 [ Task
     { taskDirectness = Direct
     , taskHypotheses = []
-    , taskConjectureLabel = Marker "first_proposition"
+    , taskConjectureLabel = Marker "prop1"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
@@ -18,7 +18,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -40,7 +40,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "second_proposition"
+    , taskConjectureLabel = Marker "prop2"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
@@ -57,7 +57,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -79,7 +79,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "third_proposition"
+    , taskConjectureLabel = Marker "prop3"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
@@ -96,7 +96,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -118,7 +118,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "fourth_proposition"
+    , taskConjectureLabel = Marker "prop4"
     , taskConjecture = Quantified Universally
         ( Scope
             ( TermSymbol
@@ -143,7 +143,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "third_proposition"
+            ( Marker "prop3"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -165,7 +165,7 @@
                 )
             )
         ,
-            ( Marker "second_proposition"
+            ( Marker "prop2"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -187,7 +187,7 @@
                 )
             )
         ,
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -209,7 +209,7 @@
                 )
             )
         ,
-            ( Marker "fourth_proposition1"
+            ( Marker "prop41"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -231,7 +231,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "fourth_proposition"
+    , taskConjectureLabel = Marker "prop4"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
@@ -248,7 +248,7 @@
     { taskDirectness = Direct
     , taskHypotheses =
         [
-            ( Marker "fourth_proposition"
+            ( Marker "prop4"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -270,7 +270,7 @@
                 )
             )
         ,
-            ( Marker "third_proposition"
+            ( Marker "prop3"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -292,7 +292,7 @@
                 )
             )
         ,
-            ( Marker "second_proposition"
+            ( Marker "prop2"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -314,7 +314,7 @@
                 )
             )
         ,
-            ( Marker "first_proposition"
+            ( Marker "prop1"
             , Quantified Universally
                 ( Scope
                     ( TermSymbol
@@ -336,7 +336,7 @@
                 )
             )
         ]
-    , taskConjectureLabel = Marker "fifth_proposition"
+    , taskConjectureLabel = Marker "prop5"
     , taskConjecture = TermSymbol
         ( SymbolPredicate
             ( PredicateRelation
diff --git a/test/golden/byRef/glossing.golden b/test/golden/byRef/glossing.golden
index e213bc9..cc7281e 100644
--- a/test/golden/byRef/glossing.golden
+++ b/test/golden/byRef/glossing.golden
@@ -5,7 +5,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "first_proposition" )
+    ( Marker "prop1" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
@@ -27,7 +27,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "second_proposition" )
+    ( Marker "prop2" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
@@ -49,7 +49,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "third_proposition" )
+    ( Marker "prop3" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
@@ -73,7 +73,7 @@
     )
     ( Qed
         ( JustificationRef
-            ( Marker "first_proposition" :| [] )
+            ( Marker "prop1" :| [] )
         )
     )
 , BlockLemma
@@ -83,7 +83,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "fourth_proposition" )
+    ( Marker "prop4" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
@@ -127,7 +127,7 @@
             )
         )
         ( JustificationRef
-            ( Marker "first_proposition" :| [] )
+            ( Marker "prop1" :| [] )
         ) ( Qed JustificationEmpty )
     )
 , BlockLemma
@@ -137,7 +137,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "fifth_proposition" )
+    ( Marker "prop5" )
     ( Lemma []
         ( TermSymbol
             ( SymbolPredicate
diff --git a/test/golden/byRef/parsing.golden b/test/golden/byRef/parsing.golden
index 2cf91b6..3df8730 100644
--- a/test/golden/byRef/parsing.golden
+++ b/test/golden/byRef/parsing.golden
@@ -5,7 +5,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "first_proposition" )
+    ( Marker "prop1" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
@@ -30,7 +30,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "second_proposition" )
+    ( Marker "prop2" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
@@ -55,7 +55,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "third_proposition" )
+    ( Marker "prop3" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
@@ -82,7 +82,7 @@
     )
     ( Qed
         ( JustificationRef
-            ( Marker "first_proposition" :| [] )
+            ( Marker "prop1" :| [] )
         )
     )
 , BlockLemma
@@ -92,7 +92,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "fourth_proposition" )
+    ( Marker "prop4" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
@@ -137,7 +137,7 @@
             )
         )
         ( JustificationRef
-            ( Marker "first_proposition" :| [] )
+            ( Marker "prop1" :| [] )
         ) ( Qed JustificationEmpty )
     )
 , BlockLemma
@@ -147,7 +147,7 @@
         , sourceColumn = Pos 1
         }
     )
-    ( Marker "fifth_proposition" )
+    ( Marker "prop5" )
     ( Lemma []
         ( StmtFormula
             ( FormulaChain
diff --git a/test/golden/byRef/tokenizing.golden b/test/golden/byRef/tokenizing.golden
index 2ae8ea6..aed896f 100644
--- a/test/golden/byRef/tokenizing.golden
+++ b/test/golden/byRef/tokenizing.golden
@@ -1,5 +1,5 @@
 [ BeginEnv "proposition"
-, Label "first_proposition"
+, Label "prop1"
 , BeginEnv "math"
 , Variable "a"
 , Symbol "="
@@ -8,7 +8,7 @@
 , Symbol "."
 , EndEnv "proposition"
 , BeginEnv "proposition"
-, Label "second_proposition"
+, Label "prop2"
 , BeginEnv "math"
 , Variable "b"
 , Symbol "="
@@ -17,7 +17,7 @@
 , Symbol "."
 , EndEnv "proposition"
 , BeginEnv "proposition"
-, Label "third_proposition"
+, Label "prop3"
 , BeginEnv "math"
 , Variable "c"
 , Symbol "="
@@ -29,11 +29,11 @@
 , Word "follows"
 , Word "by"
 , Ref
-    ( "first_proposition" :| [] )
+    ( "prop1" :| [] )
 , Symbol "."
 , EndEnv "proof"
 , BeginEnv "proposition"
-, Label "fourth_proposition"
+, Label "prop4"
 , BeginEnv "math"
 , Variable "e"
 , Symbol "="
@@ -56,11 +56,11 @@
 , EndEnv "math"
 , Word "by"
 , Ref
-    ( "first_proposition" :| [] )
+    ( "prop1" :| [] )
 , Symbol "."
 , EndEnv "proof"
 , BeginEnv "proposition"
-, Label "fifth_proposition"
+, Label "prop5"
 , BeginEnv "math"
 , Variable "f"
 , Symbol "="