2023-05-16 08:21:10 -04:00
|
|
|
import { EditorView, ViewUpdate } from '@codemirror/view'
|
2023-04-13 04:21:25 -04:00
|
|
|
import { Diagnostic, linter, lintGutter } from '@codemirror/lint'
|
|
|
|
import {
|
|
|
|
Compartment,
|
2023-06-08 04:35:51 -04:00
|
|
|
Extension,
|
2023-04-13 04:21:25 -04:00
|
|
|
RangeSet,
|
|
|
|
RangeValue,
|
|
|
|
StateEffect,
|
|
|
|
StateField,
|
|
|
|
Text,
|
|
|
|
} from '@codemirror/state'
|
|
|
|
import { Annotation } from '../../../../../types/annotation'
|
2023-09-27 05:45:49 -04:00
|
|
|
import { debugConsole } from '@/utils/debugging'
|
2023-04-13 04:21:25 -04:00
|
|
|
|
|
|
|
const compileLintSourceConf = new Compartment()
|
|
|
|
|
|
|
|
export const annotations = () => [
|
|
|
|
compileDiagnosticsState,
|
|
|
|
compileLintSourceConf.of(compileLogLintSource()),
|
2023-06-08 04:35:51 -04:00
|
|
|
/**
|
|
|
|
* The built-in lint gutter extension, configured with zero hover delay.
|
|
|
|
*/
|
2023-04-13 04:21:25 -04:00
|
|
|
lintGutter({
|
|
|
|
hoverTime: 0,
|
|
|
|
}),
|
2023-06-08 04:35:51 -04:00
|
|
|
/**
|
|
|
|
* A theme which moves the lint gutter outside the line numbers.
|
|
|
|
*/
|
2023-04-13 04:21:25 -04:00
|
|
|
EditorView.baseTheme({
|
|
|
|
'.cm-gutter-lint': {
|
|
|
|
order: -1,
|
|
|
|
},
|
|
|
|
}),
|
|
|
|
]
|
|
|
|
|
|
|
|
export const lintSourceConfig = {
|
|
|
|
delay: 100,
|
|
|
|
// Show highlights only for errors
|
|
|
|
markerFilter(diagnostics: readonly Diagnostic[]) {
|
|
|
|
return diagnostics.filter(d => d.severity === 'error')
|
|
|
|
},
|
|
|
|
// Do not show any tooltips for highlights within the editor content
|
|
|
|
tooltipFilter() {
|
|
|
|
return []
|
|
|
|
},
|
2023-05-16 08:21:10 -04:00
|
|
|
needsRefresh(update: ViewUpdate) {
|
|
|
|
return update.selectionSet
|
|
|
|
},
|
2023-04-13 04:21:25 -04:00
|
|
|
}
|
|
|
|
|
2023-06-08 04:35:51 -04:00
|
|
|
/**
|
|
|
|
* A lint source using the compile log diagnostics
|
|
|
|
*/
|
|
|
|
const compileLogLintSource = (): Extension =>
|
2023-04-13 04:21:25 -04:00
|
|
|
linter(view => {
|
|
|
|
const items: Diagnostic[] = []
|
|
|
|
const cursor = view.state.field(compileDiagnosticsState).iter()
|
|
|
|
while (cursor.value !== null) {
|
|
|
|
items.push({
|
|
|
|
...cursor.value.diagnostic,
|
|
|
|
from: cursor.from,
|
|
|
|
to: cursor.to,
|
|
|
|
})
|
|
|
|
cursor.next()
|
|
|
|
}
|
|
|
|
return items
|
|
|
|
}, lintSourceConfig)
|
|
|
|
|
|
|
|
class DiagnosticRangeValue extends RangeValue {
|
|
|
|
constructor(public diagnostic: Diagnostic) {
|
|
|
|
super()
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
const setCompileDiagnosticsEffect = StateEffect.define<Diagnostic[]>()
|
|
|
|
|
2023-06-08 04:35:51 -04:00
|
|
|
/**
|
|
|
|
* A state field for the compile log diagnostics
|
|
|
|
*/
|
2023-04-13 04:21:25 -04:00
|
|
|
export const compileDiagnosticsState = StateField.define<
|
|
|
|
RangeSet<DiagnosticRangeValue>
|
|
|
|
>({
|
|
|
|
create() {
|
|
|
|
return RangeSet.empty
|
|
|
|
},
|
|
|
|
update(value, transaction) {
|
|
|
|
for (const effect of transaction.effects) {
|
|
|
|
if (effect.is(setCompileDiagnosticsEffect)) {
|
|
|
|
return RangeSet.of(
|
|
|
|
effect.value.map(diagnostic =>
|
|
|
|
new DiagnosticRangeValue(diagnostic).range(
|
|
|
|
diagnostic.from,
|
|
|
|
diagnostic.to
|
|
|
|
)
|
|
|
|
),
|
|
|
|
true
|
|
|
|
)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
if (transaction.docChanged) {
|
|
|
|
value = value.map(transaction.changes)
|
|
|
|
}
|
|
|
|
|
|
|
|
return value
|
|
|
|
},
|
|
|
|
})
|
|
|
|
|
|
|
|
export const setAnnotations = (doc: Text, annotations: Annotation[]) => {
|
|
|
|
const diagnostics: Diagnostic[] = []
|
|
|
|
|
|
|
|
for (const annotation of annotations) {
|
|
|
|
// ignore "whole document" (row: -1) annotations
|
|
|
|
if (annotation.row !== -1) {
|
|
|
|
try {
|
|
|
|
diagnostics.push(convertAnnotationToDiagnostic(doc, annotation))
|
|
|
|
} catch (error) {
|
|
|
|
// ignore invalid annotations
|
2023-09-27 05:45:49 -04:00
|
|
|
debugConsole.debug('invalid annotation position', error)
|
2023-04-13 04:21:25 -04:00
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
return {
|
|
|
|
effects: setCompileDiagnosticsEffect.of(diagnostics),
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
export const showCompileLogDiagnostics = (show: boolean) => {
|
|
|
|
return {
|
|
|
|
effects: [
|
|
|
|
// reconfigure the compile log lint source
|
|
|
|
compileLintSourceConf.reconfigure(show ? compileLogLintSource() : []),
|
|
|
|
],
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
const convertAnnotationToDiagnostic = (
|
|
|
|
doc: Text,
|
|
|
|
annotation: Annotation
|
|
|
|
): Diagnostic => {
|
|
|
|
if (annotation.row < 0) {
|
|
|
|
throw new Error(`Invalid annotation row ${annotation.row}`)
|
|
|
|
}
|
|
|
|
|
|
|
|
const line = doc.line(annotation.row + 1)
|
|
|
|
|
|
|
|
return {
|
|
|
|
from: line.from,
|
|
|
|
to: line.to, // NOTE: highlight whole line as synctex doesn't output column number
|
|
|
|
severity: annotation.type,
|
|
|
|
message: annotation.text,
|
|
|
|
// source: annotation.source, // NOTE: the source is displayed in the tooltip
|
|
|
|
}
|
|
|
|
}
|