Skip to content
This repository was archived by the owner on Feb 26, 2021. It is now read-only.

Commit eda3e02

Browse files
committed
Merge branch 'dev' of https://github.com/banacorn/agda-mode into dev
2 parents e025bb5 + a7b0943 commit eda3e02

File tree

2 files changed

+29
-18
lines changed

2 files changed

+29
-18
lines changed

lib/view.js

Lines changed: 15 additions & 9 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

src/view.tsx

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -247,15 +247,20 @@ export default class View {
247247

248248
if (type === V.Style.Info || type === V.Style.Success) {
249249
const { banner, body } = parseContent(payload);
250-
const grouped = _.groupBy(body, 'judgementForm');
251-
this.store.dispatch(updateBanner(banner));
252-
this.store.dispatch(updateBody({
253-
goal: (grouped['goal'] || []) as V.Goal[],
254-
judgement: (grouped['type judgement'] || []) as V.Judgement[],
255-
term: (grouped['term'] || []) as V.Term[],
256-
meta: (grouped['meta'] || []) as V.Meta[],
257-
sort: (grouped['sort'] || []) as V.Sort[]
258-
}));
250+
// if parseContent failed, fallback to displaying plain text
251+
if (_.isEmpty(banner) && _.isEmpty(body)) {
252+
this.store.dispatch(updatePlainText(payload.join('\n')));
253+
} else {
254+
const grouped = _.groupBy(body, 'judgementForm');
255+
this.store.dispatch(updateBanner(banner));
256+
this.store.dispatch(updateBody({
257+
goal: (grouped['goal'] || []) as V.Goal[],
258+
judgement: (grouped['type judgement'] || []) as V.Judgement[],
259+
term: (grouped['term'] || []) as V.Term[],
260+
meta: (grouped['meta'] || []) as V.Meta[],
261+
sort: (grouped['sort'] || []) as V.Sort[]
262+
}));
263+
}
259264
} else if (type === V.Style.Error) {
260265
const error = parseError(payload.join('\n'));
261266
this.store.dispatch(updateError(error));

0 commit comments

Comments
 (0)