md: finalize syntax design for md mode

aya-prover · Dec 15, 2024 · 2908528 · 2908528
1 parent 82bd230
commit 2908528
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 11 deletions.
diff --git a/cli-impl/src/main/java/org/aya/cli/literate/AyaMdParser.java b/cli-impl/src/main/java/org/aya/cli/literate/AyaMdParser.java
@@ -65,7 +65,8 @@ public AyaMdParser(@NotNull SourceFile file, @NotNull Reporter reporter) {
     for (var attr : attrSet.getChildren()) {
       if (attr.getType() != AyaBacktickParser.ATTR) continue;
       var key = getTextInNode(attr.getChildren().getFirst());
-      var value = getTextInNode(attr.getChildren().getLast());
+      // It should be key, colon, double_quote, value, double_quote
+      var value = getTextInNode(attr.getChildren().get(attr.getChildren().size() - 2));
       if ("mode".equalsIgnoreCase(key)) {
         mode = cbt(attr, value, CodeOptions.NormalizeMode.values(), CodeOptions.NormalizeMode.NULL);
         continue;

diff --git a/cli-impl/src/test/resources/literate/hoshino-said.aya.md b/cli-impl/src/test/resources/literate/hoshino-said.aya.md
@@ -19,7 +19,7 @@ def funExt (A B : Type) (f g : A -> B) (p : Fn (a : A) -> f a = g a) : f = g =>
 def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
 ```
 
-Example: `1 = 1`(mode:NF).
+Example: `1 = 1`(mode:"full").
 
 + Aya module names are separated by `::`, not `.`.
 + Aya infers the module names automagically, using the same rule as of Haskell.

diff --git a/cli-impl/src/test/resources/literate/wow.aya.md b/cli-impl/src/test/resources/literate/wow.aya.md
@@ -34,11 +34,11 @@ Consider another example:
 def test2 {A B : Type 0} {a : A} {b : B} => wow A B a a
 ```
 
-Observe the elaborated term of `test2`: `test2`(show:core mode:full)\
-Showing the implicit arguments: `test2`(show:core mode:full implicitArgs:true)
-Showing the implicit patterns: `test2`(show:core mode:full implicitPats:true)
-Showing the lambda types: `test2`(show:core mode:full implicitArgs:true lambdaTypes:true)
-Default: `test2`(show:core mode:full)
-
-Using unknown attribute key: `test2`(hi:hello)
-Using unknown attribute value: `test2`(mode:nf)
+Observe the elaborated term of `test2`: `test2`(show:"core" mode:"full")\
+Showing the implicit arguments: `test2`(show:"core" mode:"full" implicitArgs:"true")
+Showing the implicit patterns: `test2`(show:"core" mode:"full" implicitPats:"true")
+Showing the lambda types: `test2`(show:"core" mode:"full" implicitArgs:"true" lambdaTypes:"true")
+Default: `test2`(show:"core" mode:"full")
+
+Using unknown attribute key: `test2`(hi:"hello")
+Using unknown attribute value: `test2`(mode:"nf")
diff --git a/syntax/src/main/java/org/aya/syntax/literate/AyaBacktickParser.java b/syntax/src/main/java/org/aya/syntax/literate/AyaBacktickParser.java
@@ -56,7 +56,8 @@ public class AyaBacktickParser extends BacktickParser {
 
   /**
    * Parse Aya Code Attr
-   * @param iterator the iterator which points to the first token of code span
+   *
+   * @param iterator    the iterator which points to the first token of code span
    * @param endIterator the iterator which points to the last token of code span
    * @return the iterator used for next parsing loop
    */
@@ -123,7 +124,13 @@ public class AyaBacktickParser extends BacktickParser {
     iterator = skipWS(iterator.advance());
     if (iterator.getType() != MarkdownTokenTypes.COLON) return null;
     iterator = skipWS(iterator.advance());
+
+    // Must be consecutive
+    if (iterator.getType() != MarkdownTokenTypes.DOUBLE_QUOTE) return null;
+    iterator = iterator.advance();
     if (iterator.getType() != MarkdownTokenTypes.TEXT) return null;
+    iterator = iterator.advance();
+    if (iterator.getType() != MarkdownTokenTypes.DOUBLE_QUOTE) return null;
     var endIndex = iterator.getIndex();
     return new LocalParsingResult(iterator,
       List.of(new SequentialParser.Node(new IntRange(beginIndex, endIndex + 1), ATTR))