Skip to content

Commit

Permalink
merge: #993
Browse files Browse the repository at this point in the history
993: Fix highlight lost when converting non-literal file to literal file r=imkiva a=imkiva

as  title

Co-authored-by: imkiva <imkiva@islovely.icu>
  • Loading branch information
bors[bot] and imkiva authored Aug 9, 2023
2 parents 4c9a4fd + e0ab12d commit 7295609
Show file tree
Hide file tree
Showing 3 changed files with 2 additions and 6 deletions.
2 changes: 1 addition & 1 deletion .github/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ Aya is under active development, so please expect bugs, usability or performance
+ Overlapping and order-independent patterns. Very [useful][oop] in theorem proving.
+ A literate programming mode with inline code fragment support, inspired from Agda and [1lab].
You may preview the features (in Chinese)
[here](https://blog.imkiva.org/2023/04/02/intro-literate-aya/).
[here](https://blog.imkiva.org/posts/intro-literate-aya.html).
+ Binary operators, with precedence specified by a partial ordering
(instead of a number like in Haskell or Agda)
which is useful for [equation reasoning][assoc].
Expand Down
2 changes: 1 addition & 1 deletion base/src/main/java/org/aya/concrete/GenericAyaFile.java
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,6 @@ interface Factory {
var code = originalFile().sourceCode();
var mockPos = new SourcePos(originalFile(), 0, code.length(), -1, -1, -1, -1);
// ^ we only need index, so it's fine to use a mocked line/column
return AyaLiterate.visibleAyaCodeBlock(code, mockPos);
return new AyaLiterate.AyaVisibleCodeBlock("aya", code, mockPos);
}
}
4 changes: 0 additions & 4 deletions base/src/main/java/org/aya/concrete/remark/AyaLiterate.java
Original file line number Diff line number Diff line change
Expand Up @@ -23,10 +23,6 @@ public interface AyaLiterate {
AyaHiddenCodeBlock::new);
@NotNull ImmutableSeq<InterestingLanguage<?>> AYA = ImmutableSeq.of(VISIBLE_AYA, HIDDEN_AYA);

static @NotNull Literate.CodeBlock visibleAyaCodeBlock(@NotNull String code, @NotNull SourcePos sourcePos) {
return new Literate.CodeBlock("aya", code, sourcePos);
}

class AyaCodeBlock extends Literate.CodeBlock {
public AyaCodeBlock(@NotNull String language, @NotNull String code, @Nullable SourcePos sourcePos) {
super(language, code, sourcePos);
Expand Down

0 comments on commit 7295609

Please sign in to comment.