search

banacorn / agda-mode

agda-mode on Atom
https://atom.io/packages/agda-mode
MIT License
58 stars 14 forks source link

Agda-mode dump log (Re: Issue #101) #105

Closed pdelano closed 5 years ago

pdelano commented 5 years ago

Parse Log

  1. Load

    raw text

    ``` (agda2-status-action "") (agda2-info-action "*Type-checking*" "" nil) (agda2-highlight-clear) (agda2-info-action "*Type-checking*" "Checking plfa.ExBin (/media/patrick/X:2/Projects/Agda/plfa/ExBin.agda).\n" t) (agda2-info-action "*Type-checking*" " Checking Relation.Binary.PropositionalEquality (/usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda).\n" t) (agda2-info-action "*Error*" "/usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda:240,5-5\n/usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda:240,5: Parse error\nWARNING_ON_USAGE\n Extensionality\n\"Warning: Exte..." nil) ((last . 3) . (agda2-maybe-goto '("/usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda" . 7790))) (agda2-highlight-add-annotations) (agda2-status-action "") Agda2> ```

    s-expression

    ``` ["agda2-status-action"] ``` ``` ["agda2-info-action", "*Type-checking*", "nil"] ``` ``` ["agda2-highlight-clear"] ``` ``` ["agda2-info-action", "*Type-checking*", "Checking plfa.ExBin (/media/patrick/X:2/Projects/Agda/plfa/ExBin.agda).\n", "t"] ``` ``` ["agda2-info-action", "*Type-checking*", " Checking Relation.Binary.PropositionalEquality (/usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda).\n", "t"] ``` ``` ["agda2-info-action", "*Error*", "/usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda:240,5-5\n/usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda:240,5: Parse error\nWARNING_ON_USAGE\n Extensionality\n"Warning: Exte...", "nil"] ``` ``` ["agda2-maybe-goto", ["/usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda", ".", "7790"]] ``` ``` ["agda2-highlight-add-annotations"] ``` ``` ["agda2-status-action"] ```

    response

    ``` NoStatus ``` ``` ClearRunningInfo ``` ``` ClearHighlighting ``` ``` RunningInfo 1 Checking plfa.ExBin (/media/patrick/X:2/Projects/Agda/plfa/ExBin.agda).\n ``` ``` RunningInfo 1 Checking Relation.Binary.PropositionalEquality (/usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda).\n ``` ``` DisplayInfo Error /usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda:240,5-5 /usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda:240,5: Parse error WARNING_ON_USAGE Extensionality "Warning: Exte... ``` ``` JumpToError /usr/lib/agda-stdlib-1.0.1/src/Relation/Binary/PropositionalEquality.agda 7790 ``` ``` NoStatus ```

    error

    ``` Parse error code: R1 ["agda2-highlight-add-annotations"] ```

banacorn commented 5 years ago

Interesting!

Normally agda2-highlight-add-annotations should be followed by quoted stuff like (agda2-highlight-add-annotations 'nil '(1 4 (symbol) t) Still can't figure out how Agda would emit (agda2-highlight-add-annotations), judging from the code of Agda that generates these annotations: https://github.com/agda/agda/blob/84f7ffe05e4d843713b2a2f405b3fde0c798525c/src/full/Agda/Interaction/Highlighting/Emacs.hs#L80-L88

Anyway, I'm parsing (agda2-highlight-add-annotations) as valid annotation. Thank you for posting the log!

banacorn commented 5 years ago

Fixed in v0.9.6