1use crate::capabilities::STeXSemanticTokens;
2use crate::{
3 IsLSPRange, ProgressCallbackClient,
4 state::{DocData, LSPState, UrlOrFile},
5};
6use async_lsp::lsp_types as lsp;
7use flams_math_archives::LocalArchive;
8use flams_math_archives::backend::{GlobalBackend, LocalBackend};
9use flams_stex::quickparse::stex::rules::IncludeProblemArg;
10use flams_stex::quickparse::{
11 latex::ParsedKeyValue,
12 stex::{
13 AnnotIter, DiagnosticLevel, STeXAnnot, STeXDiagnostic, STeXParseDataI,
14 rules::{
15 MathStructureArg, NotationArg, ParagraphArg, ProblemArg, SModuleArg, SymdeclArg,
16 SymdefArg, TextSymdeclArg, VardefArg,
17 },
18 structs::{
19 InlineMorphAssKind, InlineMorphAssign, ModuleOrStruct, MorphismKind, SymbolReference,
20 SymnameMode,
21 },
22 },
23};
24use flams_utils::{
25 prelude::TreeChildIter,
26 sourcerefs::{LSPLineCol, SourceRange},
27};
28use ftml_ontology::narrative::elements::paragraphs::ParagraphKind;
29use ftml_uris::{
30 ArchiveId, ArchiveUri, IsDomainUri, IsNarrativeUri, ModuleUri, SymbolUri, Uri, UriWithArchive,
31 UriWithPath,
32};
33use futures::FutureExt;
34use smallvec::SmallVec;
35
36trait AnnotExt: Sized {
37 fn as_symbol(&self) -> Option<(lsp::DocumentSymbol, &[Self])>;
38 fn links(&self, top_archive: Option<&ArchiveUri>, f: impl FnMut(lsp::DocumentLink));
39 fn goto_definition(
40 &self,
41 in_doc: &UrlOrFile,
42 pos: LSPLineCol,
43 ) -> Option<lsp::GotoDefinitionResponse>;
44 fn semantic_tokens(&self, cont: &mut impl FnMut(SourceRange<LSPLineCol>, u32));
45 fn hover(&self, top_archive: Option<&ArchiveUri>, pos: LSPLineCol) -> Option<lsp::Hover>;
46 fn inlay_hint(&self) -> Option<lsp::InlayHint>;
47 fn code_action(&self, pos: LSPLineCol, url: &lsp::Url) -> lsp::CodeActionResponse;
48}
49
50pub(crate) fn uri_from_archive_relpath(id: &ArchiveId, relpath: &str) -> Option<lsp::Url> {
51 let path = GlobalBackend.with_local_archive(id, |a| a.map(LocalArchive::source_dir))?;
52 let path = relpath.split('/').fold(path, |p, s| p.join(s));
53 lsp::Url::from_file_path(path).ok()
54}
55
56#[allow(deprecated)]
57impl AnnotExt for STeXAnnot {
58 fn as_symbol(&self) -> Option<(lsp::DocumentSymbol, &[Self])> {
59 match self {
60 Self::Module {
61 uri,
62 full_range,
63 name_range,
64 children,
65 ..
66 } => Some((
67 lsp::DocumentSymbol {
68 name: uri.to_string(),
69 detail: None,
70 kind: lsp::SymbolKind::MODULE,
71 tags: None,
72 deprecated: None,
73 range: full_range.into_range(),
74 selection_range: name_range.into_range(),
75 children: None,
76 },
77 &children,
78 )),
79 Self::MathStructure {
80 uri,
81 name_range,
82 full_range,
83 children,
84 ..
85 } => Some((
86 lsp::DocumentSymbol {
87 name: uri.uri.to_string(),
88 detail: None,
89 kind: lsp::SymbolKind::STRUCT,
90 tags: None,
91 deprecated: None,
92 range: full_range.into_range(),
93 selection_range: name_range.into_range(),
94 children: None,
95 },
96 &children,
97 )),
98 Self::ConservativeExt {
99 uri,
100 full_range,
101 extstructure_range,
102 children,
103 ..
104 } => Some((
105 lsp::DocumentSymbol {
106 name: format!("{}_EXT", uri.uri),
107 detail: None,
108 kind: lsp::SymbolKind::STRUCT,
109 tags: None,
110 deprecated: None,
111 range: full_range.into_range(),
112 selection_range: extstructure_range.into_range(),
113 children: None,
114 },
115 &children,
116 )),
117 Self::MorphismEnv {
118 full_range,
119 env_range,
120 uri,
121 children,
122 ..
123 } => Some((
124 lsp::DocumentSymbol {
125 name: uri.to_string(),
126 detail: None,
127 kind: lsp::SymbolKind::INTERFACE,
128 tags: None,
129 deprecated: None,
130 range: full_range.into_range(),
131 selection_range: env_range.into_range(),
132 children: None,
133 },
134 &children,
135 )),
136 Self::InlineMorphism {
137 full_range,
138 uri,
139 token_range,
140 ..
141 } => Some((
142 lsp::DocumentSymbol {
143 name: uri.to_string(),
144 detail: None,
145 kind: lsp::SymbolKind::INTERFACE,
146 tags: None,
147 deprecated: None,
148 range: full_range.into_range(),
149 selection_range: token_range.into_range(),
150 children: None,
151 },
152 &[],
153 )),
154 Self::Paragraph {
155 kind,
156 full_range,
157 name_range,
158 children,
159 ..
160 }
161 | Self::InlineParagraph {
162 kind,
163 full_range,
164 token_range: name_range,
165 children,
166 ..
167 } => Some((
168 lsp::DocumentSymbol {
169 name: kind.to_string(),
170 detail: None,
171 kind: lsp::SymbolKind::PACKAGE,
172 tags: None,
173 deprecated: None,
174 range: full_range.into_range(),
175 selection_range: name_range.into_range(),
176 children: None,
177 },
178 &children,
179 )),
180 Self::Problem {
181 full_range,
182 name_range,
183 children,
184 ..
185 } => Some((
186 lsp::DocumentSymbol {
187 name: "problem".to_string(),
188 detail: None,
189 kind: lsp::SymbolKind::PACKAGE,
190 tags: None,
191 deprecated: None,
192 range: full_range.into_range(),
193 selection_range: name_range.into_range(),
194 children: None,
195 },
196 &children,
197 )),
198 Self::Symdecl {
199 uri,
200 main_name_range,
201 full_range,
202 ..
203 }
204 | Self::TextSymdecl {
205 uri,
206 main_name_range,
207 full_range,
208 ..
209 }
210 | Self::Symdef {
211 uri,
212 main_name_range,
213 full_range,
214 ..
215 } => Some((
216 lsp::DocumentSymbol {
217 name: uri.uri.to_string(),
218 detail: None,
219 kind: lsp::SymbolKind::OBJECT,
220 tags: None,
221 deprecated: None,
222 range: full_range.into_range(),
223 selection_range: main_name_range.into_range(),
224 children: None,
225 },
226 &[],
227 )),
228 Self::Vardef {
229 name,
230 main_name_range,
231 full_range,
232 ..
233 } => Some((
234 lsp::DocumentSymbol {
235 name: name.to_string(),
236 detail: None,
237 kind: lsp::SymbolKind::VARIABLE,
238 tags: None,
239 deprecated: None,
240 range: full_range.into_range(),
241 selection_range: main_name_range.into_range(),
242 children: None,
243 },
244 &[],
245 )),
246 Self::Varseq {
247 name,
248 main_name_range,
249 full_range,
250 ..
251 } => Some((
252 lsp::DocumentSymbol {
253 name: name.to_string(),
254 detail: None,
255 kind: lsp::SymbolKind::VARIABLE,
256 tags: None,
257 deprecated: None,
258 range: full_range.into_range(),
259 selection_range: main_name_range.into_range(),
260 children: None,
261 },
262 &[],
263 )),
264 Self::ImportModule {
265 module, full_range, ..
266 } => Some((
267 lsp::DocumentSymbol {
268 name: format!("import@{}", module.uri),
269 detail: Some(module.uri.to_string()),
270 kind: lsp::SymbolKind::PACKAGE,
271 tags: None,
272 deprecated: None,
273 range: full_range.into_range(),
274 selection_range: full_range.into_range(),
275 children: None,
276 },
277 &[],
278 )),
279 Self::UseModule {
280 module, full_range, ..
281 } => Some((
282 lsp::DocumentSymbol {
283 name: format!("usemodule@{}", module.uri),
284 detail: Some(module.uri.to_string()),
285 kind: lsp::SymbolKind::PACKAGE,
286 tags: None,
287 deprecated: None,
288 range: full_range.into_range(),
289 selection_range: full_range.into_range(),
290 children: None,
291 },
292 &[],
293 )),
294 Self::UseStructure {
295 structure,
296 full_range,
297 ..
298 } => Some((
299 lsp::DocumentSymbol {
300 name: format!("usestructure@{}", structure.uri),
301 detail: None,
302 kind: lsp::SymbolKind::PACKAGE,
303 tags: None,
304 deprecated: None,
305 range: full_range.into_range(),
306 selection_range: full_range.into_range(),
307 children: None,
308 },
309 &[],
310 )),
311 Self::SetMetatheory {
312 module, full_range, ..
313 } => Some((
314 lsp::DocumentSymbol {
315 name: format!("metatheory@{}", module.uri),
316 detail: Some(module.uri.to_string()),
317 kind: lsp::SymbolKind::NAMESPACE,
318 tags: None,
319 deprecated: None,
320 range: full_range.into_range(),
321 selection_range: full_range.into_range(),
322 children: None,
323 },
324 &[],
325 )),
326 Self::Inputref {
327 archive,
328 filepath,
329 full_range: range,
330 ..
331 }
332 | Self::IncludeProblem {
333 archive,
334 filepath,
335 full_range: range,
336 ..
337 } => Some((
338 lsp::DocumentSymbol {
339 name: archive.as_ref().map_or_else(
340 || format!("inputref@{}", filepath.0),
341 |(a, _)| format!("inputref@[{a}]{}", filepath.0),
342 ),
343 detail: None,
344 kind: lsp::SymbolKind::PACKAGE,
345 tags: None,
346 deprecated: None,
347 range: range.into_range(),
348 selection_range: range.into_range(),
349 children: None,
350 },
351 &[],
352 )),
353 Self::MHInput {
354 archive,
355 filepath,
356 full_range: range,
357 ..
358 } => Some((
359 lsp::DocumentSymbol {
360 name: archive.as_ref().map_or_else(
361 || format!("mhinput@{}", filepath.0),
362 |(a, _)| format!("mhinput@[{a}]{}", filepath.0),
363 ),
364 detail: None,
365 kind: lsp::SymbolKind::PACKAGE,
366 tags: None,
367 deprecated: None,
368 range: range.into_range(),
369 selection_range: range.into_range(),
370 children: None,
371 },
372 &[],
373 )),
374 Self::MHGraphics { .. }
375 | Self::SemanticMacro { .. }
376 | Self::VariableMacro { .. }
377 | Self::SymName { .. }
378 | Self::Symref { .. }
379 | Self::Notation { .. }
380 | Self::Svar { .. }
381 | Self::Symuse { .. }
382 | Self::Definiens { .. }
383 | Self::Defnotation { .. }
384 | Self::RenameDecl { .. }
385 | Self::Precondition { .. }
386 | Self::Objective { .. }
387 | Self::Assign { .. } => None,
388 }
389 }
390
391 fn links(&self, top_archive: Option<&ArchiveUri>, mut cont: impl FnMut(lsp::DocumentLink)) {
392 match self {
393 Self::IncludeProblem {
394 archive, filepath, ..
395 } => {
396 let Some(a) = archive
397 .as_ref()
398 .map_or_else(|| top_archive.map(ArchiveUri::archive_id), |(a, _)| Some(a))
399 else {
400 return;
401 };
402 let Some(uri) = uri_from_archive_relpath(a, &filepath.0) else {
403 return;
404 };
405 cont(lsp::DocumentLink {
406 range: filepath.1.into_range(),
407 target: Some(uri),
408 tooltip: None,
409 data: None,
410 });
411 }
412 Self::MHGraphics {
413 archive, filepath, ..
414 } => {
415 let Some(a) = archive.as_ref().map_or_else(
416 || top_archive.map(UriWithArchive::archive_id),
417 |(a, _)| Some(a),
418 ) else {
419 return;
420 };
421 let Some(uri) = uri_from_archive_relpath(a, &filepath.0) else {
422 return;
423 };
424 cont(lsp::DocumentLink {
425 range: filepath.1.into_range(),
426 target: Some(uri),
427 tooltip: None,
428 data: None,
429 });
430 }
431 Self::Inputref {
432 archive,
433 token_range,
434 filepath,
435 full_range: range,
436 ..
437 }
438 | Self::MHInput {
439 archive,
440 token_range,
441 filepath,
442 full_range: range,
443 ..
444 } => {
445 let Some(a) = archive.as_ref().map_or_else(
446 || top_archive.map(UriWithArchive::archive_id),
447 |(a, _)| Some(a),
448 ) else {
449 return;
450 };
451 let Some(uri) = uri_from_archive_relpath(a, &filepath.0) else {
452 return;
453 };
454 let mut range = *range;
455 range.start = token_range.end;
456 cont(lsp::DocumentLink {
457 range: range.into_range(),
458 target: Some(uri),
459 tooltip: None,
460 data: None,
461 });
462 }
463 Self::ImportModule { .. }
464 | Self::UseModule { .. }
465 | Self::SemanticMacro { .. }
466 | Self::VariableMacro { .. }
467 | Self::SetMetatheory { .. }
468 | Self::Module { .. }
469 | Self::MathStructure { .. }
470 | Self::Symdecl { .. }
471 | Self::TextSymdecl { .. }
472 | Self::SymName { .. }
473 | Self::Symref { .. }
474 | Self::Notation { .. }
475 | Self::Symdef { .. }
476 | Self::Vardef { .. }
477 | Self::Paragraph { .. }
478 | Self::Symuse { .. }
479 | Self::Svar { .. }
480 | Self::Varseq { .. }
481 | Self::Definiens { .. }
482 | Self::Defnotation { .. }
483 | Self::ConservativeExt { .. }
484 | Self::UseStructure { .. }
485 | Self::InlineParagraph { .. }
486 | Self::Problem { .. }
487 | Self::MorphismEnv { .. }
488 | Self::RenameDecl { .. }
489 | Self::Precondition { .. }
490 | Self::Objective { .. }
491 | Self::Assign { .. }
492 | Self::InlineMorphism { .. } => (),
493 }
494 }
495
496 fn goto_definition(
497 &self,
498 in_doc: &UrlOrFile,
499 pos: LSPLineCol,
500 ) -> Option<lsp::GotoDefinitionResponse> {
501 macro_rules! here {
502 ($r:expr) => {
503 Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
504 uri: in_doc.clone().into(),
505 range: SourceRange::into_range($r),
506 }))
507 };
508 }
509 match self {
510 Self::Module { name_range, .. } => {
511 if !name_range.contains(pos) {
512 return None;
513 };
514 here!(*name_range)
515 }
516 Self::MathStructure {
517 extends,
518 name_range,
519 opts,
520 ..
521 } => {
522 if name_range.contains(pos) {
523 return here!(*name_range);
524 }
525 for o in opts {
526 if let MathStructureArg::Name(range, _) = o {
527 if range.contains(pos) {
528 return here!(*range);
529 }
530 }
531 }
532 extends.iter().find_map(|(uri, r)| {
533 if r.contains(pos) {
534 let Some(p) = &uri.filepath else { return None };
535 let Ok(url) = lsp::Url::from_file_path(p) else {
536 return None;
537 };
538 Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
540 uri: url,
541 range: SourceRange::into_range(uri.range),
542 }))
543 } else {
544 None
545 }
546 })
547 }
548 Self::MorphismEnv {
549 domain_range,
550 name_range,
551 domain,
552 ..
553 } => {
554 if name_range.contains(pos) {
555 return here!(*name_range);
556 }
557 if domain_range.contains(pos) {
558 let Some((p, range)) = (match domain {
559 ModuleOrStruct::Module(uri) => {
560 uri.full_path.as_ref().map(|r| (r, SourceRange::default()))
561 }
562 ModuleOrStruct::Struct(uri) => {
563 uri.filepath.as_ref().map(|r| (r, uri.range))
564 }
565 }) else {
566 return None;
567 };
568 let Ok(url) = lsp::Url::from_file_path(p) else {
569 return None;
570 };
571 return Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
572 uri: url,
573 range: SourceRange::into_range(range),
574 }));
575 } else {
576 None
577 }
578 }
579 Self::InlineMorphism {
580 domain_range,
581 domain,
582 assignments,
583 name_range,
584 ..
585 } => {
586 if name_range.contains(pos) {
587 return here!(*name_range);
588 }
589 if domain_range.contains(pos) {
590 let Some((p, range)) = (match domain {
591 ModuleOrStruct::Module(uri) => {
592 uri.full_path.as_ref().map(|r| (r, SourceRange::default()))
593 }
594 ModuleOrStruct::Struct(uri) => {
595 uri.filepath.as_ref().map(|r| (r, uri.range))
596 }
597 }) else {
598 return None;
599 };
600 let Ok(url) = lsp::Url::from_file_path(p) else {
601 return None;
602 };
603 return Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
604 uri: url,
605 range: SourceRange::into_range(range),
606 }));
607 }
608 for a in assignments {
609 if a.symbol_range.contains(pos) {
610 let Some(p) = &a.symbol.filepath else {
611 return None;
612 };
613 let Ok(url) = lsp::Url::from_file_path(p) else {
614 return None;
615 };
616 return Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
617 uri: url,
618 range: SourceRange::into_range(a.symbol_range),
619 }));
620 }
621 if let Some((_, InlineMorphAssKind::Rename(_, _, r))) = &a.first {
622 if r.contains(pos) {
623 return here!(*r);
624 }
625 }
626 if let Some((_, InlineMorphAssKind::Rename(_, _, r))) = &a.second {
627 if r.contains(pos) {
628 return here!(*r);
629 }
630 }
631 }
632 None
633 }
634 Self::Paragraph { parsed_args, .. } | Self::InlineParagraph { parsed_args, .. } => {
635 for p in parsed_args {
636 match p {
637 ParagraphArg::Fors(ParsedKeyValue { val_range, val, .. }) => {
638 if val_range.contains(pos) {
639 for (s, r) in val {
640 if r.contains(pos) {
641 let Some(p) =
642 &s.first().unwrap_or_else(|| unreachable!()).filepath
643 else {
644 return None;
645 };
646 let Ok(url) = lsp::Url::from_file_path(p) else {
647 return None;
648 };
649 return Some(lsp::GotoDefinitionResponse::Scalar(
651 lsp::Location {
652 uri: url,
653 range: SourceRange::into_range(
654 s.first()
655 .unwrap_or_else(|| unreachable!())
656 .range,
657 ),
658 },
659 ));
660 }
661 }
662 }
663 return None;
664 }
665 ParagraphArg::Name(ParsedKeyValue { val_range, .. })
666 | ParagraphArg::MacroName(ParsedKeyValue { val_range, .. })
667 if val_range.contains(pos) =>
668 {
669 return here!(*val_range);
670 }
671 _ => (),
672 }
673 }
674 None
675 }
676 Self::Symdecl {
677 main_name_range,
678 parsed_args,
679 ..
680 } => {
681 if main_name_range.contains(pos) {
682 return here!(*main_name_range);
683 }
684 for a in parsed_args {
685 if let SymdeclArg::Name(ParsedKeyValue { val_range, .. }) = a {
686 if val_range.contains(pos) {
687 return here!(*val_range);
688 }
689 }
690 }
691 None
692 }
693 Self::TextSymdecl {
694 main_name_range,
695 parsed_args,
696 ..
697 } => {
698 if main_name_range.contains(pos) {
699 return here!(*main_name_range);
700 }
701 for a in parsed_args {
702 if let TextSymdeclArg::Name(ParsedKeyValue { val_range, .. }) = a {
703 if val_range.contains(pos) {
704 return here!(*val_range);
705 }
706 }
707 }
708 None
709 }
710 Self::Symdef {
711 main_name_range,
712 parsed_args,
713 ..
714 } => {
715 if main_name_range.contains(pos) {
716 return here!(*main_name_range);
717 }
718 for a in parsed_args {
719 if let SymdefArg::Name(ParsedKeyValue { val_range, .. }) = a {
720 if val_range.contains(pos) {
721 return here!(*val_range);
722 }
723 }
724 }
725 None
726 }
727 Self::RenameDecl {
728 uri,
729 orig_range,
730 name_range,
731 macroname_range,
732 ..
733 } => {
734 if let Some(name_range) = name_range {
735 if name_range.contains(pos) {
736 return here!(*name_range);
737 }
738 }
739 if macroname_range.contains(pos) {
740 return here!(*macroname_range);
741 }
742 if !orig_range.contains(pos) {
743 return None;
744 };
745 let Some(p) = &uri.filepath else { return None };
746 let Ok(url) = lsp::Url::from_file_path(p) else {
747 return None;
748 };
749 Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
751 uri: url,
752 range: SourceRange::into_range(uri.range),
753 }))
754 }
755 Self::Vardef {
756 main_name_range,
757 parsed_args,
758 ..
759 }
760 | Self::Varseq {
761 main_name_range,
762 parsed_args,
763 ..
764 } => {
765 if main_name_range.contains(pos) {
766 return here!(*main_name_range);
767 }
768 for a in parsed_args {
769 if let VardefArg::Name(ParsedKeyValue { val_range, .. }) = a {
770 if val_range.contains(pos) {
771 return here!(*val_range);
772 }
773 }
774 }
775 None
776 }
777
778 Self::ImportModule {
779 module,
780 archive_range,
781 path_range,
782 ..
783 }
784 | Self::UseModule {
785 module,
786 archive_range,
787 path_range,
788 ..
789 }
790 | Self::SetMetatheory {
791 archive_range,
792 path_range,
793 module,
794 ..
795 } => {
796 let range = archive_range.map_or(*path_range, |a| SourceRange {
797 start: a.start,
798 end: path_range.end,
799 });
800 if !range.contains(pos) {
801 return None;
802 };
803 let Some(p) = module.full_path.as_ref() else {
804 return None;
805 };
806 let Ok(uri) = lsp::Url::from_file_path(p) else {
807 return None;
808 };
809 Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
810 uri,
811 range: lsp::Range::default(),
812 }))
813 }
814 Self::ConservativeExt { ext_range, uri, .. } => {
815 if !ext_range.contains(pos) {
816 return None;
817 };
818 let Some(p) = &uri.filepath else { return None };
819 let Ok(url) = lsp::Url::from_file_path(p) else {
820 return None;
821 };
822 Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
824 uri: url,
825 range: SourceRange::into_range(uri.range),
826 }))
827 }
828 Self::SymName {
829 uri,
830 name_range: range,
831 ..
832 }
833 | Self::Symref {
834 uri,
835 name_range: range,
836 ..
837 }
838 | Self::Notation {
839 uri,
840 name_range: range,
841 ..
842 }
843 | Self::Symuse {
844 uri,
845 name_range: range,
846 ..
847 }
848 | Self::Precondition {
849 uri,
850 symbol_range: range,
851 ..
852 }
853 | Self::Objective {
854 uri,
855 symbol_range: range,
856 ..
857 }
858 | Self::Definiens {
859 uri,
860 name_range: Some(range),
861 ..
862 } => {
863 if !range.contains(pos) {
864 return None;
865 };
866 let Some(p) = &uri.first().unwrap_or_else(|| unreachable!()).filepath else {
867 return None;
868 };
869 let Ok(url) = lsp::Url::from_file_path(p) else {
870 return None;
871 };
872 Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
874 uri: url,
875 range: SourceRange::into_range(
876 uri.first().unwrap_or_else(|| unreachable!()).range,
877 ),
878 }))
879 }
880 Self::SemanticMacro {
881 uri,
882 token_range: range,
883 ..
884 }
885 | Self::UseStructure {
886 structure: uri,
887 structure_range: range,
888 ..
889 }
890 | Self::Assign {
891 uri,
892 orig_range: range,
893 ..
894 } => {
895 if !range.contains(pos) {
896 return None;
897 };
898 let Some(p) = &uri.filepath else { return None };
899 let Ok(url) = lsp::Url::from_file_path(p) else {
900 return None;
901 };
902 Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
904 uri: url,
905 range: SourceRange::into_range(uri.range),
906 }))
907 }
908 Self::VariableMacro {
909 orig, full_range, ..
910 } => {
911 if !full_range.contains(pos) {
912 return None;
913 };
914 Some(lsp::GotoDefinitionResponse::Scalar(lsp::Location {
915 uri: in_doc.clone().into(),
916 range: SourceRange::into_range(*orig),
917 }))
918 }
919 Self::Svar { .. }
920 | Self::Inputref { .. }
921 | Self::IncludeProblem { .. }
922 | Self::MHGraphics { .. }
923 | Self::MHInput { .. }
924 | Self::Problem { .. }
925 | Self::Definiens { .. }
926 | Self::Defnotation { .. } => None,
927 }
928 }
929 fn semantic_tokens(&self, cont: &mut impl FnMut(SourceRange<LSPLineCol>, u32)) {
930 match self {
931 Self::Module {
932 name_range,
933 full_range,
934 smodule_range,
935 opts,
936 children,
937 ..
938 } => {
939 cont(*smodule_range, STeXSemanticTokens::DECLARATION);
940 for o in opts {
941 match o {
942 SModuleArg::Title(v) => {
943 cont(v.key_range, STeXSemanticTokens::KEYWORD);
944 for e in &v.val {
945 e.semantic_tokens(cont);
946 }
947 }
948 SModuleArg::Sig(ParsedKeyValue {
949 key_range,
950 val_range,
951 ..
952 }) => {
953 cont(*key_range, STeXSemanticTokens::KEYWORD);
954 cont(*val_range, STeXSemanticTokens::KEYWORD);
955 }
956 SModuleArg::Meta(ParsedKeyValue { key_range, .. }) => {
959 cont(*key_range, STeXSemanticTokens::KEYWORD);
960 }
961 }
962 }
963 cont(*name_range, STeXSemanticTokens::NAME);
964 for c in children {
965 c.semantic_tokens(cont);
966 }
967 let mut end_range = *full_range;
968 end_range.end.col -= 1;
969 end_range.start.line = end_range.end.line;
970 end_range.start.col = end_range.end.col - "smodule".len() as u32;
971 cont(end_range, STeXSemanticTokens::DECLARATION);
972 }
973 Self::MathStructure {
974 extends,
975 name_range,
976 opts,
977 full_range,
978 children,
979 mathstructure_range,
980 ..
981 } => {
982 cont(*mathstructure_range, STeXSemanticTokens::DECLARATION);
983 cont(*name_range, STeXSemanticTokens::NAME);
984 for o in opts {
985 match o {
986 MathStructureArg::This(ParsedKeyValue { key_range, val, .. }) => {
987 cont(*key_range, STeXSemanticTokens::KEYWORD);
988 for e in val {
989 e.semantic_tokens(cont);
990 }
991 }
992 MathStructureArg::Name(range, _) => {
993 cont(*range, STeXSemanticTokens::NAME);
994 }
995 }
996 }
997 for (_, r) in extends {
998 cont(*r, STeXSemanticTokens::SYMBOL)
999 }
1000 for c in children {
1001 c.semantic_tokens(cont);
1002 }
1003 let mut end_range = *full_range;
1004 end_range.end.col -= 1;
1005 end_range.start.line = end_range.end.line;
1006 let s = if extends.is_empty() {
1007 "mathstructure"
1008 } else {
1009 "extstructure"
1010 };
1011 end_range.start.col = end_range.end.col - s.len() as u32;
1012 cont(end_range, STeXSemanticTokens::DECLARATION);
1013 }
1014 Self::ConservativeExt {
1015 ext_range,
1016 full_range,
1017 extstructure_range,
1018 children,
1019 ..
1020 } => {
1021 cont(*extstructure_range, STeXSemanticTokens::DECLARATION);
1022 cont(*ext_range, STeXSemanticTokens::SYMBOL);
1023 for c in children {
1024 c.semantic_tokens(cont);
1025 }
1026 let mut end_range = *full_range;
1027 end_range.end.col -= 1;
1028 end_range.start.line = end_range.end.line;
1029 end_range.start.col = end_range.end.col - "extstructure*".len() as u32;
1030 cont(end_range, STeXSemanticTokens::DECLARATION);
1031 }
1032 Self::MorphismEnv {
1033 env_range,
1034 star,
1035 kind,
1036 name_range,
1037 domain_range,
1038 full_range,
1039 domain,
1040 children,
1041 ..
1042 } => {
1043 cont(*env_range, STeXSemanticTokens::DECLARATION);
1044 cont(*name_range, STeXSemanticTokens::NAME);
1045 match domain {
1046 ModuleOrStruct::Struct(_) => cont(*domain_range, STeXSemanticTokens::SYMBOL),
1047 _ => (),
1048 }
1049 for c in children {
1050 c.semantic_tokens(cont);
1051 }
1052
1053 let mut end_range = *full_range;
1054 end_range.end.col -= 1;
1055 end_range.start.line = end_range.end.line;
1056 let len = match kind {
1057 MorphismKind::CopyModule => "copymodule".len(),
1058 MorphismKind::InterpretModule => "interpretmodule".len(),
1059 };
1060 let len = if *star { len + 1 } else { len };
1061 end_range.start.col = end_range.end.col - len as u32;
1062 cont(end_range, STeXSemanticTokens::DECLARATION);
1063 }
1064 Self::InlineMorphism {
1065 token_range,
1066 name_range,
1067 domain_range,
1068 domain,
1069 assignments,
1070 ..
1071 } => {
1072 cont(*token_range, STeXSemanticTokens::DECLARATION);
1073 cont(*name_range, STeXSemanticTokens::NAME);
1074 match domain {
1075 ModuleOrStruct::Struct(_) => cont(*domain_range, STeXSemanticTokens::SYMBOL),
1076 _ => (),
1077 }
1078 for InlineMorphAssign {
1079 first,
1080 second,
1081 symbol_range,
1082 ..
1083 } in assignments
1084 {
1085 cont(*symbol_range, STeXSemanticTokens::SYMBOL);
1086 if let Some((e, knd)) = first {
1087 let end = LSPLineCol {
1088 line: e.line,
1089 col: e.col + 1,
1090 };
1091 let range = SourceRange { start: *e, end };
1092 cont(range, STeXSemanticTokens::KEYWORD);
1093 match knd {
1094 InlineMorphAssKind::Df(v) => {
1095 for c in v {
1096 c.semantic_tokens(cont);
1097 }
1098 }
1099 InlineMorphAssKind::Rename(mn, _, n) => {
1100 if let Some((_, mn)) = mn {
1101 cont(*mn, STeXSemanticTokens::NAME);
1102 }
1103 cont(*n, STeXSemanticTokens::NAME);
1104 }
1105 }
1106 }
1107 if let Some((e, knd)) = second {
1108 let end = LSPLineCol {
1109 line: e.line,
1110 col: e.col + 1,
1111 };
1112 let range = SourceRange { start: *e, end };
1113 cont(range, STeXSemanticTokens::KEYWORD);
1114 match knd {
1115 InlineMorphAssKind::Df(v) => {
1116 for c in v {
1117 c.semantic_tokens(cont);
1118 }
1119 }
1120 InlineMorphAssKind::Rename(mn, _, n) => {
1121 if let Some((_, mn)) = mn {
1122 cont(*mn, STeXSemanticTokens::NAME);
1123 }
1124 cont(*n, STeXSemanticTokens::NAME);
1125 }
1126 }
1127 }
1128 }
1129 }
1130 Self::UseModule { token_range, .. } => cont(*token_range, STeXSemanticTokens::LOCAL),
1131 Self::UseStructure {
1132 token_range,
1133 structure_range,
1134 ..
1135 } => {
1136 cont(*token_range, STeXSemanticTokens::LOCAL);
1137 cont(*structure_range, STeXSemanticTokens::SYMBOL);
1138 }
1139 Self::IncludeProblem {
1140 token_range, args, ..
1141 } => {
1142 cont(*token_range, STeXSemanticTokens::REF_MACRO);
1143 for a in args {
1144 let r = match a {
1145 IncludeProblemArg::Min(m) => m.key_range,
1146 IncludeProblemArg::Pts(m) => m.key_range,
1147 IncludeProblemArg::Archive(m) => m.key_range,
1148 };
1149 cont(r, STeXSemanticTokens::KEYWORD);
1150 }
1151 }
1152 Self::Inputref {
1153 token_range: range, ..
1154 }
1155 | Self::MHInput {
1156 token_range: range, ..
1157 }
1158 | Self::MHGraphics {
1159 token_range: range, ..
1160 }
1161 | Self::Defnotation { full_range: range } => {
1162 cont(*range, STeXSemanticTokens::REF_MACRO)
1163 }
1164 Self::SetMetatheory { token_range, .. } | Self::ImportModule { token_range, .. } => {
1165 cont(*token_range, STeXSemanticTokens::DECLARATION)
1166 }
1167 Self::SemanticMacro { token_range, .. } => {
1168 cont(*token_range, STeXSemanticTokens::SYMBOL)
1169 }
1170 Self::VariableMacro { token_range, .. } => {
1171 cont(*token_range, STeXSemanticTokens::VARIABLE)
1172 }
1173 Self::Problem {
1174 full_range,
1175 name_range,
1176 parsed_args,
1177 children,
1178 ..
1179 } => {
1180 cont(*name_range, STeXSemanticTokens::REF_MACRO);
1181 for e in parsed_args {
1182 match e {
1183 ProblemArg::Autogradable(ParsedKeyValue {
1188 key_range,
1189 val_range,
1190 ..
1191 }) => {
1192 cont(*key_range, STeXSemanticTokens::KEYWORD);
1193 cont(*val_range, STeXSemanticTokens::KEYWORD);
1194 }
1195 ProblemArg::Style(ParsedKeyValue { key_range, .. })
1196 | ProblemArg::Pts(ParsedKeyValue { key_range, .. })
1197 | ProblemArg::Min(ParsedKeyValue { key_range, .. })
1198 | ProblemArg::Id(ParsedKeyValue { key_range, .. }) => {
1199 cont(*key_range, STeXSemanticTokens::KEYWORD)
1200 }
1201 ProblemArg::Title(ParsedKeyValue { key_range, val, .. }) => {
1202 cont(*key_range, STeXSemanticTokens::KEYWORD);
1203 for c in val {
1204 c.semantic_tokens(cont);
1205 }
1206 }
1207 }
1208 }
1209 for c in children {
1210 c.semantic_tokens(cont);
1211 }
1212 let mut end_range = *full_range;
1213 end_range.end.col -= 1;
1214 end_range.start.line = end_range.end.line;
1215 cont(end_range, STeXSemanticTokens::REF_MACRO);
1216 }
1217 Self::Paragraph {
1218 kind,
1219 symbol,
1220 name_range,
1221 parsed_args,
1222 children,
1223 full_range,
1224 ..
1225 } => {
1226 if symbol.is_some() {
1227 cont(*name_range, STeXSemanticTokens::DECLARATION);
1228 } else {
1229 cont(*name_range, STeXSemanticTokens::REF_MACRO);
1230 }
1231 for e in parsed_args {
1232 match e {
1233 ParagraphArg::Tp(ParsedKeyValue { key_range, val, .. })
1234 | ParagraphArg::Df(ParsedKeyValue { key_range, val, .. })
1235 | ParagraphArg::Return(ParsedKeyValue { key_range, val, .. })
1236 | ParagraphArg::Argtypes(ParsedKeyValue { key_range, val, .. })
1237 | ParagraphArg::Title(ParsedKeyValue { key_range, val, .. }) => {
1238 cont(*key_range, STeXSemanticTokens::KEYWORD);
1239 for c in val {
1240 c.semantic_tokens(cont);
1241 }
1242 }
1243 ParagraphArg::Args(ParsedKeyValue {
1244 key_range,
1245 val_range,
1246 ..
1247 }) => {
1248 cont(*key_range, STeXSemanticTokens::KEYWORD);
1249 cont(*val_range, STeXSemanticTokens::KEYWORD);
1250 }
1251 ParagraphArg::Name(ParsedKeyValue {
1252 key_range,
1253 val_range,
1254 ..
1255 })
1256 | ParagraphArg::MacroName(ParsedKeyValue {
1257 key_range,
1258 val_range,
1259 ..
1260 }) => {
1261 cont(*key_range, STeXSemanticTokens::KEYWORD);
1262 cont(*val_range, STeXSemanticTokens::NAME);
1263 }
1264 ParagraphArg::Style(ParsedKeyValue { key_range, .. })
1265 | ParagraphArg::Assoc(ParsedKeyValue { key_range, .. })
1266 | ParagraphArg::Role(ParsedKeyValue { key_range, .. })
1267 | ParagraphArg::Reorder(ParsedKeyValue { key_range, .. })
1268 | ParagraphArg::From(ParsedKeyValue { key_range, .. })
1269 | ParagraphArg::To(ParsedKeyValue { key_range, .. })
1270 | ParagraphArg::Judgment(ParsedKeyValue { key_range, .. })
1271 | ParagraphArg::Id(ParsedKeyValue { key_range, .. }) => {
1272 cont(*key_range, STeXSemanticTokens::KEYWORD)
1273 }
1274 ParagraphArg::Fors(ParsedKeyValue { key_range, val, .. }) => {
1275 cont(*key_range, STeXSemanticTokens::KEYWORD);
1276 for (_, f) in val {
1277 cont(*f, STeXSemanticTokens::SYMBOL);
1278 }
1279 }
1280 }
1281 }
1282 for c in children {
1283 c.semantic_tokens(cont);
1284 }
1285 let mut end_range = *full_range;
1286 end_range.end.col -= 1;
1287 end_range.start.line = end_range.end.line;
1288 let parname = match kind {
1289 ParagraphKind::Definition => "sdefinition".len(),
1290 ParagraphKind::Paragraph => "sparagraph".len(),
1291 ParagraphKind::Proof => "sproof".len(),
1292 ParagraphKind::Example => "sexample".len(),
1293 ParagraphKind::Assertion => "sassertion".len(),
1294 _ => return,
1295 };
1296 end_range.start.col = end_range.end.col - parname as u32;
1297 if symbol.is_some() {
1298 cont(end_range, STeXSemanticTokens::DECLARATION);
1299 } else {
1300 cont(end_range, STeXSemanticTokens::REF_MACRO);
1301 }
1302 }
1303 Self::InlineParagraph {
1304 symbol,
1305 token_range,
1306 parsed_args,
1307 children,
1308 ..
1309 } => {
1310 if symbol.is_some() {
1311 cont(*token_range, STeXSemanticTokens::DECLARATION);
1312 } else {
1313 cont(*token_range, STeXSemanticTokens::REF_MACRO);
1314 }
1315 for e in parsed_args {
1316 match e {
1317 ParagraphArg::Tp(ParsedKeyValue { key_range, val, .. })
1318 | ParagraphArg::Df(ParsedKeyValue { key_range, val, .. })
1319 | ParagraphArg::Return(ParsedKeyValue { key_range, val, .. })
1320 | ParagraphArg::Argtypes(ParsedKeyValue { key_range, val, .. })
1321 | ParagraphArg::Title(ParsedKeyValue { key_range, val, .. }) => {
1322 cont(*key_range, STeXSemanticTokens::KEYWORD);
1323 for c in val {
1324 c.semantic_tokens(cont);
1325 }
1326 }
1327 ParagraphArg::Args(ParsedKeyValue {
1328 key_range,
1329 val_range,
1330 ..
1331 }) => {
1332 cont(*key_range, STeXSemanticTokens::KEYWORD);
1333 cont(*val_range, STeXSemanticTokens::KEYWORD);
1334 }
1335 ParagraphArg::Name(ParsedKeyValue {
1336 key_range,
1337 val_range,
1338 ..
1339 })
1340 | ParagraphArg::MacroName(ParsedKeyValue {
1341 key_range,
1342 val_range,
1343 ..
1344 }) => {
1345 cont(*key_range, STeXSemanticTokens::KEYWORD);
1346 cont(*val_range, STeXSemanticTokens::NAME);
1347 }
1348 ParagraphArg::Style(ParsedKeyValue { key_range, .. })
1349 | ParagraphArg::Assoc(ParsedKeyValue { key_range, .. })
1350 | ParagraphArg::Role(ParsedKeyValue { key_range, .. })
1351 | ParagraphArg::Reorder(ParsedKeyValue { key_range, .. })
1352 | ParagraphArg::Judgment(ParsedKeyValue { key_range, .. })
1353 | ParagraphArg::From(ParsedKeyValue { key_range, .. })
1354 | ParagraphArg::To(ParsedKeyValue { key_range, .. })
1355 | ParagraphArg::Id(ParsedKeyValue { key_range, .. }) => {
1356 cont(*key_range, STeXSemanticTokens::KEYWORD)
1357 }
1358 ParagraphArg::Fors(ParsedKeyValue { key_range, val, .. }) => {
1359 cont(*key_range, STeXSemanticTokens::KEYWORD);
1360 for (_, f) in val {
1361 cont(*f, STeXSemanticTokens::SYMBOL);
1362 }
1363 }
1364 }
1365 }
1366 for c in children {
1367 c.semantic_tokens(cont);
1368 }
1369 }
1370 Self::Symdecl {
1371 main_name_range,
1372 token_range,
1373 parsed_args,
1374 ..
1375 } => {
1376 cont(*token_range, STeXSemanticTokens::DECLARATION);
1377 cont(*main_name_range, STeXSemanticTokens::NAME);
1378
1379 for e in parsed_args {
1380 match e {
1381 SymdeclArg::Tp(ParsedKeyValue { key_range, val, .. })
1382 | SymdeclArg::Df(ParsedKeyValue { key_range, val, .. })
1383 | SymdeclArg::Return(ParsedKeyValue { key_range, val, .. })
1384 | SymdeclArg::Argtypes(ParsedKeyValue { key_range, val, .. }) => {
1385 cont(*key_range, STeXSemanticTokens::KEYWORD);
1386 for c in val {
1387 c.semantic_tokens(cont);
1388 }
1389 }
1390 SymdeclArg::Args(ParsedKeyValue {
1391 key_range,
1392 val_range,
1393 ..
1394 }) => {
1395 cont(*key_range, STeXSemanticTokens::KEYWORD);
1396 cont(*val_range, STeXSemanticTokens::KEYWORD);
1397 }
1398 SymdeclArg::Name(ParsedKeyValue {
1399 key_range,
1400 val_range,
1401 ..
1402 }) => {
1403 cont(*key_range, STeXSemanticTokens::KEYWORD);
1404 cont(*val_range, STeXSemanticTokens::NAME);
1405 }
1406 SymdeclArg::Style(ParsedKeyValue { key_range, .. })
1407 | SymdeclArg::Assoc(ParsedKeyValue { key_range, .. })
1408 | SymdeclArg::Role(ParsedKeyValue { key_range, .. })
1409 | SymdeclArg::Reorder(ParsedKeyValue { key_range, .. }) => {
1410 cont(*key_range, STeXSemanticTokens::KEYWORD)
1411 }
1412 }
1413 }
1414 }
1415 Self::TextSymdecl {
1416 main_name_range,
1417 token_range,
1418 parsed_args,
1419 ..
1420 } => {
1421 cont(*token_range, STeXSemanticTokens::DECLARATION);
1422 cont(*main_name_range, STeXSemanticTokens::NAME);
1423
1424 for e in parsed_args {
1425 match e {
1426 TextSymdeclArg::Tp(ParsedKeyValue { key_range, val, .. })
1427 | TextSymdeclArg::Df(ParsedKeyValue { key_range, val, .. }) => {
1428 cont(*key_range, STeXSemanticTokens::KEYWORD);
1429 for c in val {
1430 c.semantic_tokens(cont);
1431 }
1432 }
1433 TextSymdeclArg::Name(ParsedKeyValue {
1434 key_range,
1435 val_range,
1436 ..
1437 }) => {
1438 cont(*key_range, STeXSemanticTokens::KEYWORD);
1439 cont(*val_range, STeXSemanticTokens::NAME);
1440 }
1441 TextSymdeclArg::Style(ParsedKeyValue { key_range, .. }) => {
1442 cont(*key_range, STeXSemanticTokens::KEYWORD)
1443 }
1444 }
1445 }
1446 }
1447 Self::Symdef {
1448 main_name_range,
1449 token_range,
1450 parsed_args,
1451 ..
1452 } => {
1453 cont(*token_range, STeXSemanticTokens::DECLARATION);
1454 cont(*main_name_range, STeXSemanticTokens::NAME);
1455
1456 for e in parsed_args {
1457 match e {
1458 SymdefArg::Tp(ParsedKeyValue { key_range, val, .. })
1459 | SymdefArg::Df(ParsedKeyValue { key_range, val, .. })
1460 | SymdefArg::Return(ParsedKeyValue { key_range, val, .. })
1461 | SymdefArg::Op(ParsedKeyValue { key_range, val, .. })
1462 | SymdefArg::Argtypes(ParsedKeyValue { key_range, val, .. }) => {
1463 cont(*key_range, STeXSemanticTokens::KEYWORD);
1464 for c in val {
1465 c.semantic_tokens(cont);
1466 }
1467 }
1468 SymdefArg::Args(ParsedKeyValue {
1469 key_range,
1470 val_range,
1471 ..
1472 }) => {
1473 cont(*key_range, STeXSemanticTokens::KEYWORD);
1474 cont(*val_range, STeXSemanticTokens::KEYWORD);
1475 }
1476 SymdefArg::Name(ParsedKeyValue {
1477 key_range,
1478 val_range,
1479 ..
1480 }) => {
1481 cont(*key_range, STeXSemanticTokens::KEYWORD);
1482 cont(*val_range, STeXSemanticTokens::NAME);
1483 }
1484 SymdefArg::Id(v, _) => cont(*v, STeXSemanticTokens::NAME),
1485 SymdefArg::Style(ParsedKeyValue { key_range, .. })
1486 | SymdefArg::Assoc(ParsedKeyValue { key_range, .. })
1487 | SymdefArg::Role(ParsedKeyValue { key_range, .. })
1488 | SymdefArg::Prec(ParsedKeyValue { key_range, .. })
1489 | SymdefArg::Reorder(ParsedKeyValue { key_range, .. }) => {
1490 cont(*key_range, STeXSemanticTokens::KEYWORD)
1491 }
1492 }
1493 }
1494 }
1495 Self::RenameDecl {
1496 token_range,
1497 orig_range,
1498 name_range,
1499 macroname_range,
1500 ..
1501 } => {
1502 cont(*token_range, STeXSemanticTokens::DECLARATION);
1503 cont(*orig_range, STeXSemanticTokens::SYMBOL);
1504 if let Some(n) = name_range {
1505 cont(*n, STeXSemanticTokens::NAME);
1506 }
1507 cont(*macroname_range, STeXSemanticTokens::NAME);
1508 }
1509 Self::Assign {
1510 token_range,
1511 orig_range,
1512 ..
1513 } => {
1514 cont(*token_range, STeXSemanticTokens::DECLARATION);
1515 cont(*orig_range, STeXSemanticTokens::SYMBOL);
1516 }
1517 Self::Svar { full_range, .. } => cont(*full_range, STeXSemanticTokens::VARIABLE),
1518 Self::Vardef {
1519 main_name_range,
1520 token_range,
1521 parsed_args,
1522 ..
1523 }
1524 | Self::Varseq {
1525 main_name_range,
1526 token_range,
1527 parsed_args,
1528 ..
1529 } => {
1530 cont(*token_range, STeXSemanticTokens::LOCAL);
1531 cont(*main_name_range, STeXSemanticTokens::NAME);
1532
1533 for e in parsed_args {
1534 match e {
1535 VardefArg::Tp(ParsedKeyValue { key_range, val, .. })
1536 | VardefArg::Df(ParsedKeyValue { key_range, val, .. })
1537 | VardefArg::Return(ParsedKeyValue { key_range, val, .. })
1538 | VardefArg::Op(ParsedKeyValue { key_range, val, .. })
1539 | VardefArg::Argtypes(ParsedKeyValue { key_range, val, .. }) => {
1540 cont(*key_range, STeXSemanticTokens::KEYWORD);
1541 for c in val {
1542 c.semantic_tokens(cont);
1543 }
1544 }
1545 VardefArg::Args(ParsedKeyValue {
1546 key_range,
1547 val_range,
1548 ..
1549 }) => {
1550 cont(*key_range, STeXSemanticTokens::KEYWORD);
1551 cont(*val_range, STeXSemanticTokens::KEYWORD);
1552 }
1553 VardefArg::Name(ParsedKeyValue {
1554 key_range,
1555 val_range,
1556 ..
1557 }) => {
1558 cont(*key_range, STeXSemanticTokens::KEYWORD);
1559 cont(*val_range, STeXSemanticTokens::NAME);
1560 }
1561 VardefArg::Id(v, _) => cont(*v, STeXSemanticTokens::NAME),
1562 VardefArg::Style(ParsedKeyValue { key_range, .. })
1563 | VardefArg::Assoc(ParsedKeyValue { key_range, .. })
1564 | VardefArg::Role(ParsedKeyValue { key_range, .. })
1565 | VardefArg::Prec(ParsedKeyValue { key_range, .. })
1566 | VardefArg::Bind(ParsedKeyValue { key_range, .. })
1567 | VardefArg::Reorder(ParsedKeyValue { key_range, .. }) => {
1568 cont(*key_range, STeXSemanticTokens::KEYWORD)
1569 }
1570 }
1571 }
1572 }
1573 Self::Notation {
1574 token_range,
1575 name_range,
1576 notation_args,
1577 ..
1578 } => {
1579 cont(*token_range, STeXSemanticTokens::DECLARATION);
1580 cont(*name_range, STeXSemanticTokens::SYMBOL);
1581 for e in notation_args {
1582 match e {
1583 NotationArg::Op(ParsedKeyValue { key_range, val, .. }) => {
1584 cont(*key_range, STeXSemanticTokens::KEYWORD);
1585 for c in val {
1586 c.semantic_tokens(cont);
1587 }
1588 }
1589 NotationArg::Id(v, _) => cont(*v, STeXSemanticTokens::NAME),
1590 NotationArg::Prec(ParsedKeyValue { key_range, .. }) => {
1591 cont(*key_range, STeXSemanticTokens::KEYWORD)
1592 }
1593 }
1594 }
1595 }
1596 Self::SymName {
1597 token_range,
1598 name_range,
1599 ..
1600 }
1601 | Self::Symref {
1602 token_range,
1603 name_range,
1604 ..
1605 }
1606 | Self::Symuse {
1607 token_range,
1608 name_range,
1609 ..
1610 } => {
1611 cont(*token_range, STeXSemanticTokens::REF_MACRO);
1612 cont(*name_range, STeXSemanticTokens::SYMBOL);
1613 }
1614 Self::Precondition {
1615 token_range,
1616 dim_range,
1617 symbol_range,
1618 ..
1619 }
1620 | Self::Objective {
1621 token_range,
1622 dim_range,
1623 symbol_range,
1624 ..
1625 } => {
1626 cont(*token_range, STeXSemanticTokens::REF_MACRO);
1627 cont(*dim_range, STeXSemanticTokens::KEYWORD);
1628 cont(*symbol_range, STeXSemanticTokens::SYMBOL);
1629 }
1630 Self::Definiens {
1631 token_range,
1632 name_range,
1633 ..
1634 } => {
1635 cont(*token_range, STeXSemanticTokens::REF_MACRO);
1636 if let Some(r) = name_range {
1637 cont(*r, STeXSemanticTokens::SYMBOL);
1638 }
1639 }
1640 }
1641 }
1642
1643 fn hover(&self, top_archive: Option<&ArchiveUri>, pos: LSPLineCol) -> Option<lsp::Hover> {
1644 fn uriname(pre: &str, d: &impl std::fmt::Display) -> String {
1645 format!("{pre}<sup>`{d}`</sup>")
1646 }
1647 match self {
1649 Self::SymName {
1650 uri,
1651 name_range: range,
1652 ..
1653 }
1654 | Self::Symref {
1655 uri,
1656 name_range: range,
1657 ..
1658 }
1659 | Self::Notation {
1660 uri,
1661 name_range: range,
1662 ..
1663 }
1664 | Self::Symuse {
1665 uri,
1666 name_range: range,
1667 ..
1668 }
1669 | Self::Precondition {
1670 uri,
1671 symbol_range: range,
1672 ..
1673 }
1674 | Self::Objective {
1675 uri,
1676 symbol_range: range,
1677 ..
1678 }
1679 | Self::Definiens {
1680 uri,
1681 name_range: Some(range),
1682 ..
1683 } => Some(lsp::Hover {
1684 range: Some(SourceRange::into_range(*range)),
1685 contents: lsp::HoverContents::Markup(lsp::MarkupContent {
1686 kind: lsp::MarkupKind::Markdown,
1687 value: uriname("", &uri.first().unwrap_or_else(|| unreachable!()).uri),
1688 }),
1689 }),
1690 Self::SemanticMacro {
1691 uri,
1692 full_range: range,
1693 ..
1694 }
1695 | Self::ConservativeExt {
1696 uri,
1697 ext_range: range,
1698 ..
1699 }
1700 | Self::UseStructure {
1701 structure: uri,
1702 structure_range: range,
1703 ..
1704 }
1705 | Self::MorphismEnv {
1706 domain: ModuleOrStruct::Struct(uri),
1707 domain_range: range,
1708 ..
1709 }
1710 | Self::RenameDecl {
1711 uri,
1712 orig_range: range,
1713 ..
1714 }
1715 | Self::Assign {
1716 uri,
1717 orig_range: range,
1718 ..
1719 } => Some(lsp::Hover {
1720 range: Some(SourceRange::into_range(*range)),
1721 contents: lsp::HoverContents::Markup(lsp::MarkupContent {
1722 kind: lsp::MarkupKind::Markdown,
1723 value: uriname("", &uri.uri),
1724 }),
1725 }),
1726 Self::InlineMorphism {
1727 domain_range,
1728 domain,
1729 assignments,
1730 ..
1731 } => {
1732 if domain_range.contains(pos) {
1733 let uri = match domain {
1734 ModuleOrStruct::Struct(sym) => &sym.uri,
1735 _ => return None,
1736 };
1737 return Some(lsp::Hover {
1738 range: Some(SourceRange::into_range(*domain_range)),
1739 contents: lsp::HoverContents::Markup(lsp::MarkupContent {
1740 kind: lsp::MarkupKind::Markdown,
1741 value: uriname("", uri),
1742 }),
1743 });
1744 }
1745 for a in assignments {
1746 if a.symbol_range.contains(pos) {
1747 return Some(lsp::Hover {
1748 range: Some(SourceRange::into_range(a.symbol_range)),
1749 contents: lsp::HoverContents::Markup(lsp::MarkupContent {
1750 kind: lsp::MarkupKind::Markdown,
1751 value: uriname("", &a.symbol.uri),
1752 }),
1753 });
1754 }
1755 }
1756 None
1757 }
1758 Self::Svar {
1759 full_range, name, ..
1760 }
1761 | Self::VariableMacro {
1762 name, full_range, ..
1763 } => Some(lsp::Hover {
1764 range: Some(SourceRange::into_range(*full_range)),
1765 contents: lsp::HoverContents::Markup(lsp::MarkupContent {
1766 kind: lsp::MarkupKind::Markdown,
1767 value: uriname("Variable ", name),
1768 }),
1769 }),
1770 Self::MathStructure { extends, .. } => extends.iter().find_map(|(s, r)| {
1771 if r.contains(pos) {
1772 Some(lsp::Hover {
1773 range: Some(SourceRange::into_range(*r)),
1774 contents: lsp::HoverContents::Markup(lsp::MarkupContent {
1775 kind: lsp::MarkupKind::Markdown,
1776 value: uriname("", &s.uri),
1777 }),
1778 })
1779 } else {
1780 None
1781 }
1782 }),
1783 Self::Paragraph { parsed_args, .. } | Self::InlineParagraph { parsed_args, .. } => {
1784 for p in parsed_args {
1785 if let ParagraphArg::Fors(ParsedKeyValue { val_range, val, .. }) = p {
1786 if val_range.contains(pos) {
1787 for (s, r) in val {
1788 if r.contains(pos) {
1789 return Some(lsp::Hover {
1790 range: Some(SourceRange::into_range(*r)),
1791 contents: lsp::HoverContents::Markup(lsp::MarkupContent {
1792 kind: lsp::MarkupKind::Markdown,
1793 value: uriname(
1794 "",
1795 &s.first().unwrap_or_else(|| unreachable!()).uri,
1796 ),
1797 }),
1798 });
1799 }
1800 }
1801 }
1802 return None;
1803 }
1804 }
1805 None
1806 }
1807 Self::MHGraphics {
1808 filepath,
1809 archive,
1810 full_range,
1811 ..
1812 } => {
1813 let Some(a) = archive.as_ref().map_or_else(
1814 || top_archive.map(UriWithArchive::archive_id),
1815 |(a, _)| Some(a),
1816 ) else {
1817 return None;
1818 };
1819 let Some(uri) = uri_from_archive_relpath(a, &filepath.0) else {
1820 return None;
1821 };
1822 Some(lsp::Hover {
1823 range: Some(SourceRange::into_range(*full_range)),
1824 contents: lsp::HoverContents::Markup(lsp::MarkupContent {
1825 kind: lsp::MarkupKind::Markdown,
1826 value: format!(""),
1827 }),
1828 })
1829 }
1830 Self::Module {
1831 uri,
1832 name_range,
1833 full_range,
1834 ..
1835 } => {
1836 let range = SourceRange {
1837 start: full_range.start,
1838 end: name_range.end,
1839 };
1840 Some(lsp::Hover {
1841 range: Some(SourceRange::into_range(range)),
1842 contents: lsp::HoverContents::Markup(lsp::MarkupContent {
1843 kind: lsp::MarkupKind::Markdown,
1844 value: uri.to_string(),
1845 }),
1846 })
1847 }
1848 Self::ImportModule { .. }
1849 | Self::UseModule { .. }
1850 | Self::SetMetatheory { .. }
1851 | Self::Inputref { .. }
1852 | Self::IncludeProblem { .. }
1853 | Self::MHInput { .. }
1854 | Self::Symdecl { .. }
1855 | Self::Symdef { .. }
1856 | Self::Vardef { .. }
1857 | Self::Varseq { .. }
1858 | Self::Definiens { .. }
1859 | Self::TextSymdecl { .. }
1860 | Self::Problem { .. }
1861 | Self::Defnotation { .. }
1862 | Self::MorphismEnv { .. } => None,
1863 }
1864 }
1865 fn inlay_hint(&self) -> Option<lsp::InlayHint> {
1866 match self {
1867 Self::SymName {
1868 uri,
1869 full_range,
1870 mode: mod_,
1871 ..
1872 } => {
1873 let name = uri
1874 .first()
1875 .unwrap_or_else(|| unreachable!())
1876 .uri
1877 .name()
1878 .last();
1879 let name = match mod_ {
1880 SymnameMode::Cap {
1881 post: Some((_, _, post)),
1882 } => {
1883 let cap = name.chars().next().unwrap().to_uppercase().to_string();
1884 format!("={cap}{}{post}", &name[1..])
1885 }
1886 SymnameMode::Cap { .. } => {
1887 let cap = name.chars().next().unwrap().to_uppercase().to_string();
1888 format!("={cap}{}", &name[1..])
1889 }
1890 SymnameMode::PostS {
1891 pre: Some((_, _, pre)),
1892 } => format!("={pre}{name}s"),
1893 SymnameMode::PostS { .. } => format!("={name}s"),
1894 SymnameMode::CapAndPostS => {
1895 let cap = name.chars().next().unwrap().to_uppercase().to_string();
1896 format!("={cap}{}s", &name[1..])
1897 }
1898 SymnameMode::PrePost {
1899 pre: Some((_, _, pre)),
1900 post: Some((_, _, post)),
1901 } => format!("={pre}{name}{post}"),
1902 SymnameMode::PrePost {
1903 pre: Some((_, _, pre)),
1904 ..
1905 } => format!("={pre}{name}"),
1906 SymnameMode::PrePost {
1907 post: Some((_, _, post)),
1908 ..
1909 } => format!("={name}{post}"),
1910 _ => format!("={name}"),
1911 };
1912 Some(lsp::InlayHint {
1913 position: SourceRange::into_range(*full_range).end,
1914 label: lsp::InlayHintLabel::String(name),
1915 kind: Some(lsp::InlayHintKind::PARAMETER),
1916 text_edits: None,
1917 tooltip: None,
1918 padding_left: None,
1919 padding_right: None,
1920 data: None,
1921 })
1922 }
1923 Self::Definiens {
1924 uri,
1925 name_range: None,
1926 full_range,
1927 ..
1928 } => Some(lsp::InlayHint {
1929 position: SourceRange::into_range(*full_range).end,
1930 label: lsp::InlayHintLabel::String(format!(
1931 "[{}]",
1932 uri.first().unwrap_or_else(|| unreachable!()).uri.name()
1933 )),
1934 kind: Some(lsp::InlayHintKind::PARAMETER),
1935 text_edits: None,
1936 tooltip: None,
1937 padding_left: None,
1938 padding_right: None,
1939 data: None,
1940 }),
1941 _ => None,
1942 }
1943 }
1944 fn code_action(&self, pos: LSPLineCol, url: &lsp::Url) -> lsp::CodeActionResponse {
1945 fn from_syms(
1946 url: &lsp::Url,
1947 v: &[SymbolReference<LSPLineCol>],
1948 r: SourceRange<LSPLineCol>,
1949 ) -> lsp::CodeActionResponse {
1950 fn disamb(uri: &SymbolUri, all: &[String]) -> String {
1951 let mut ret = format!("?{}", uri.name());
1952 if all.iter().filter(|s| s.ends_with(&ret)).count() == 1 {
1953 return ret;
1954 }
1955 ret = format!("?{}{ret}", uri.module_name());
1956 if all.iter().filter(|s| s.ends_with(&ret)).count() == 1 {
1957 return ret;
1958 }
1959 if let Some(path) = uri.path() {
1960 let mut had_path = false;
1961 for s in path.steps().rev() {
1962 if had_path {
1963 ret = format!("{s}/{ret}");
1964 } else {
1965 had_path = true;
1966 ret = format!("{s}{ret}");
1967 }
1968 if all.iter().filter(|s| s.ends_with(&ret)).count() == 1 {
1969 return ret;
1970 }
1971 }
1972 }
1973 for i in uri.archive_id().steps().rev() {
1974 ret = format!("{i}/{ret}");
1975 if all.iter().filter(|s| s.ends_with(&ret)).count() == 1 {
1976 return ret;
1977 }
1978 }
1979 ret
1980 }
1981 let all_strs: SmallVec<_, 2> = v
1982 .iter()
1983 .map(|u| {
1984 let mut ret = u.uri.archive_id().to_string();
1985 if let Some(p) = u.uri.path() {
1986 ret.push('/');
1987 ret.push_str(&p.to_string());
1988 }
1989 ret.push_str(&format!("?{}?{}", u.uri.module_name(), u.uri.name()));
1990 ret
1991 })
1992 .collect();
1993 v.iter()
1994 .map(|u| {
1995 let disam = disamb(&u.uri, &all_strs);
1996 let mut edits = std::collections::HashMap::default();
1997 edits.insert(
1998 url.clone(),
1999 vec![lsp::TextEdit {
2000 range: SourceRange::into_range(r),
2001 new_text: disam.clone(),
2002 }],
2003 );
2004 lsp::CodeActionOrCommand::CodeAction(lsp::CodeAction {
2005 title: disam,
2006 kind: Some(lsp::CodeActionKind::QUICKFIX),
2007 diagnostics: None,
2008 edit: Some(lsp::WorkspaceEdit {
2009 document_changes: None,
2010 changes: Some(edits),
2011 change_annotations: None,
2012 }),
2013 command: None,
2014 is_preferred: None,
2015 disabled: None,
2016 data: None,
2017 })
2018 })
2019 .collect()
2020 }
2021 match self {
2022 Self::Notation {
2023 uri, name_range, ..
2024 }
2025 | Self::SymName {
2026 uri, name_range, ..
2027 }
2028 | Self::Symuse {
2029 uri, name_range, ..
2030 }
2031 | Self::Symref {
2032 uri, name_range, ..
2033 }
2034 | Self::Precondition {
2035 uri,
2036 symbol_range: name_range,
2037 ..
2038 }
2039 | Self::Objective {
2040 uri,
2041 symbol_range: name_range,
2042 ..
2043 }
2044 | Self::Definiens {
2045 uri,
2046 name_range: Some(name_range),
2047 ..
2048 } => {
2049 if !name_range.contains(pos) {
2050 return Vec::new();
2051 }
2052 if uri.len() > 1 {
2053 from_syms(url, uri, *name_range)
2054 } else {
2055 Vec::new()
2056 }
2057 }
2058
2059 Self::Paragraph { parsed_args, .. } | Self::InlineParagraph { parsed_args, .. } => {
2060 let fors = parsed_args.iter().find_map(|a| {
2061 if let ParagraphArg::Fors(ls) = a {
2062 Some(ls)
2063 } else {
2064 None
2065 }
2066 });
2067 if let Some(fors) = fors {
2068 for (s, r) in &fors.val {
2069 if !r.contains(pos) {
2070 continue;
2071 }
2072 if s.len() > 1 {
2073 return from_syms(url, s, *r);
2074 }
2075 return Vec::new();
2076 }
2077 Vec::new()
2078 } else {
2079 Vec::new()
2080 }
2081 }
2082
2083 Self::Problem { .. }
2084 | Self::Module { .. }
2085 | Self::MathStructure { .. }
2086 | Self::ConservativeExt { .. }
2087 | Self::MorphismEnv { .. }
2088 | Self::InlineMorphism { .. }
2089 | Self::SemanticMacro { .. }
2090 | Self::VariableMacro { .. }
2091 | Self::Svar { .. }
2092 | Self::ImportModule { .. }
2093 | Self::UseModule { .. }
2094 | Self::UseStructure { .. }
2095 | Self::SetMetatheory { .. }
2096 | Self::Inputref { .. }
2097 | Self::IncludeProblem { .. }
2098 | Self::MHGraphics { .. }
2099 | Self::MHInput { .. }
2100 | Self::Symdecl { .. }
2101 | Self::TextSymdecl { .. }
2102 | Self::RenameDecl { .. }
2103 | Self::Symdef { .. }
2104 | Self::Vardef { .. }
2105 | Self::Varseq { .. }
2106 | Self::Defnotation { .. }
2107 | Self::Definiens { .. }
2108 | Self::Assign { .. } => Vec::new(),
2109 }
2110 }
2111}
2112
2113impl LSPState {
2114 #[must_use]
2115 pub fn get_diagnostics(
2116 &self,
2117 uri: &UrlOrFile,
2118 progress: Option<ProgressCallbackClient>,
2119 ) -> Option<impl std::future::Future<Output = lsp::DocumentDiagnosticReportResult> + use<>>
2120 {
2121 fn default() -> lsp::DocumentDiagnosticReportResult {
2122 lsp::DocumentDiagnosticReportResult::Report(lsp::DocumentDiagnosticReport::Full(
2123 lsp::RelatedFullDocumentDiagnosticReport::default(),
2124 ))
2125 }
2126 let d = self.get(uri)?;
2127 let slf = self.clone();
2128 Some(async move {
2129 d.with_annots(slf, |data| {
2130 let diags = &data.diagnostics;
2131 let r = lsp::DocumentDiagnosticReportResult::Report(
2132 lsp::DocumentDiagnosticReport::Full(lsp::RelatedFullDocumentDiagnosticReport {
2133 related_documents: None,
2134 full_document_diagnostic_report: lsp::FullDocumentDiagnosticReport {
2135 result_id: None,
2136 items: diags.iter().map(to_diagnostic).collect(),
2137 },
2138 }),
2139 );
2140 tracing::trace!("diagnostics: {:?}", r);
2141 if let Some(p) = progress {
2142 p.finish()
2143 }
2144 r
2145 })
2146 .await
2147 .unwrap_or_else(default)
2148 })
2149 }
2150
2151 #[must_use]
2152 pub fn get_symbols(
2153 &self,
2154 uri: &UrlOrFile,
2155 progress: Option<ProgressCallbackClient>,
2156 ) -> Option<impl std::future::Future<Output = Option<lsp::DocumentSymbolResponse>> + use<>>
2157 {
2158 #[allow(deprecated)]
2159 fn to_symbols(v: &[STeXAnnot]) -> Vec<lsp::DocumentSymbol> {
2160 let mut curr = v.iter();
2161 let mut ret = Vec::new();
2162 let mut stack = Vec::new();
2163 loop {
2165 if let Some(e) = curr.next() {
2166 if let Some((mut symbol, children)) = e.as_symbol() {
2167 if children.is_empty() {
2168 ret.push(symbol)
2169 } else {
2170 let old = std::mem::replace(&mut curr, children.iter());
2171 symbol.children = Some(std::mem::take(&mut ret));
2172 stack.push((old, symbol));
2173 }
2174 }
2175 } else if let Some((i, mut s)) = stack.pop() {
2176 curr = i;
2177 std::mem::swap(
2178 &mut ret,
2179 s.children.as_mut().unwrap_or_else(|| unreachable!()),
2180 );
2181 ret.push(s);
2182 } else {
2183 break;
2184 }
2185 }
2186 ret
2188 }
2189
2190 let d = self.get(uri)?;
2191 let slf = self.clone();
2192 Some(d.with_annots(slf, |data| {
2193 let r = lsp::DocumentSymbolResponse::Nested(to_symbols(&data.annotations));
2194 tracing::trace!("document symbols: {:?}", r);
2195 if let Some(p) = progress {
2196 p.finish()
2197 }
2198 r
2199 }))
2200 }
2201
2202 #[must_use]
2203 pub fn get_links(
2204 &self,
2205 uri: &UrlOrFile,
2206 progress: Option<ProgressCallbackClient>,
2207 ) -> Option<impl std::future::Future<Output = Option<Vec<lsp::DocumentLink>>> + use<>> {
2208 let d = self.get(uri)?;
2209 let da = d.archive().cloned();
2210 let slf = self.clone();
2211 Some(d.with_annots(slf, move |data| {
2212 let mut ret = Vec::new();
2213 let iter: AnnotIter = data.annotations.iter().into();
2214 for e in <AnnotIter as TreeChildIter<STeXAnnot>>::dfs(iter) {
2215 e.links(da.as_ref(), |l| ret.push(l));
2216 }
2217 if let Some(p) = progress {
2219 p.finish()
2220 }
2221 ret
2222 }))
2223 }
2224
2225 pub fn prepare_module_hierarchy(
2226 &self,
2227 uri: UrlOrFile,
2228 _: Option<ProgressCallbackClient>,
2229 ) -> Option<impl std::future::Future<Output = Option<Vec<lsp::CallHierarchyItem>>> + use<>>
2230 {
2231 let d = self.get(&uri)?;
2232 let url: lsp::Url = uri.into();
2233 d.document_uri().map(|doc| {
2234 std::future::ready(Some(vec![lsp::CallHierarchyItem {
2235 name: format!("{}.{}", doc.document_name(), doc.language()),
2236 kind: lsp::SymbolKind::FILE,
2237 tags: None,
2238 detail: None,
2239 uri: url.clone(),
2240 range: lsp::Range::default(), selection_range: lsp::Range::default(),
2242 data: Some(doc.to_string().into()),
2243 }]))
2244 })
2245 }
2246
2247 pub fn module_hierarchy_imports(
2248 &self,
2249 url: lsp::Url,
2250 kind: lsp::SymbolKind,
2251 uri: Uri,
2252 _: Option<ProgressCallbackClient>,
2253 ) -> Option<
2254 impl std::future::Future<Output = Option<Vec<lsp::CallHierarchyIncomingCall>>> + use<>,
2255 > {
2256 Some(std::future::ready({
2257 let url = url.into();
2258 let d = self.documents.read().get(&url).cloned()?;
2259 let annots = match d {
2260 DocData::Doc(d) => d.annotations,
2261 DocData::Data(d, _) => d,
2262 };
2263 let data = annots.lock();
2264 let mut rets = Vec::new();
2265 let (chs, usemods) = if kind == lsp::SymbolKind::FILE {
2266 (&*data.annotations, true)
2267 } else {
2268 let mut iter: AnnotIter = data.annotations.iter().into();
2269 (
2270 iter.find_map(|e| match e {
2271 STeXAnnot::Module {
2272 uri: muri,
2273 children,
2274 ..
2275 } if matches!(&uri,Uri::Module(u) if u == muri) => Some(&**children),
2276 STeXAnnot::MathStructure {
2277 uri: suri,
2278 children,
2279 extends,
2280 ..
2281 } if matches!(&uri,Uri::Symbol(u) if u == &suri.uri) => {
2282 for (sym, range) in extends {
2283 if let Some(p) = sym.filepath.as_ref() {
2284 let Ok(url) = lsp::Url::from_file_path(p) else {
2285 continue;
2286 };
2287 rets.push(lsp::CallHierarchyIncomingCall {
2288 from_ranges: vec![IsLSPRange::into_range(*range)],
2289 from: lsp::CallHierarchyItem {
2290 name: sym.uri.name().to_string(),
2291 detail: Some(
2292 sym.uri
2293 .to_string()
2294 .split_once("a=")
2295 .unwrap_or_else(|| unreachable!())
2296 .1
2297 .to_string(),
2298 ),
2299 kind: lsp::SymbolKind::STRUCT,
2300 tags: None,
2301 uri: url,
2302 range: lsp::Range::default(),
2303 selection_range: lsp::Range::default(),
2304 data: Some(sym.uri.to_string().into()),
2305 },
2306 });
2307 }
2308 }
2309 Some(&**children)
2310 }
2311 _ => None,
2312 })?,
2313 false,
2314 )
2315 };
2316 let iter: AnnotIter = chs.iter().into();
2317 for e in <AnnotIter as TreeChildIter<STeXAnnot>>::dfs(iter) {
2318 match e {
2319 STeXAnnot::ImportModule {
2320 module, full_range, ..
2321 } if !usemods => {
2322 let Some(p) = module.full_path.as_ref() else {
2323 continue;
2324 };
2325 let Ok(url) = lsp::Url::from_file_path(p) else {
2326 continue;
2327 };
2328 rets.push(lsp::CallHierarchyIncomingCall {
2329 from_ranges: vec![lsp::Range::default()],
2330 from: lsp::CallHierarchyItem {
2331 detail: Some(
2332 module
2333 .uri
2334 .to_string()
2335 .split_once("a=")
2336 .unwrap_or_else(|| unreachable!())
2337 .1
2338 .to_string(),
2339 ),
2340 name: module.uri.module_name().to_string(),
2341 kind: lsp::SymbolKind::CLASS,
2342 tags: None,
2343 uri: url,
2344 range: IsLSPRange::into_range(*full_range),
2345 selection_range: IsLSPRange::into_range(*full_range),
2346 data: Some(module.uri.to_string().into()),
2347 },
2348 })
2349 }
2350 STeXAnnot::Module {
2351 uri,
2352 name_range,
2353 full_range,
2354 ..
2355 } if usemods => rets.push(lsp::CallHierarchyIncomingCall {
2356 from_ranges: vec![IsLSPRange::into_range(*full_range)],
2357 from: lsp::CallHierarchyItem {
2358 detail: Some(
2359 uri.to_string()
2360 .split_once("a=")
2361 .unwrap_or_else(|| unreachable!())
2362 .1
2363 .to_string(),
2364 ),
2365 name: uri.module_name().to_string(),
2366 kind: lsp::SymbolKind::MODULE,
2367 tags: None,
2368 uri: url.clone().into(),
2369 range: IsLSPRange::into_range(*full_range),
2370 selection_range: IsLSPRange::into_range(*name_range),
2371 data: Some(uri.to_string().into()),
2372 },
2373 }),
2374 STeXAnnot::UseModule {
2375 module, full_range, ..
2376 } if usemods => {
2377 let Some(p) = module.full_path.as_ref() else {
2378 continue;
2379 };
2380 let Ok(url) = lsp::Url::from_file_path(p) else {
2381 continue;
2382 };
2383 rets.push(lsp::CallHierarchyIncomingCall {
2384 from_ranges: vec![lsp::Range::default()],
2385 from: lsp::CallHierarchyItem {
2386 detail: Some(
2387 module
2388 .uri
2389 .to_string()
2390 .split_once("a=")
2391 .unwrap_or_else(|| unreachable!())
2392 .1
2393 .to_string(),
2394 ),
2395 name: module.uri.module_name().to_string(),
2396 kind: lsp::SymbolKind::METHOD,
2397 tags: None,
2398 uri: url,
2399 range: IsLSPRange::into_range(*full_range),
2400 selection_range: IsLSPRange::into_range(*full_range),
2401 data: Some(module.uri.to_string().into()),
2402 },
2403 })
2404 }
2405 _ => (),
2406 }
2407 }
2408 Some(rets)
2409 }))
2410 }
2411
2412 #[must_use]
2413 pub fn get_references(
2414 &self,
2415 uri: UrlOrFile,
2416 position: lsp::Position,
2417 _: Option<ProgressCallbackClient>,
2418 ) -> Option<impl std::future::Future<Output = Option<Vec<lsp::Location>>> + use<>> {
2419 let d = self.get(&uri)?;
2420 let pos = LSPLineCol {
2421 line: position.line,
2422 col: position.character,
2423 };
2424 let slf = self.clone();
2425 enum Target {
2426 Module(ModuleUri),
2427 Structure(SymbolUri),
2428 Symbol(SymbolUri),
2429 Morphism(SymbolUri),
2430 }
2431 Some(async move {
2432 let e = d
2433 .with_annots(slf.clone(), move |data| match at_position(data, pos)? {
2434 STeXAnnot::Module { uri, .. } => Some(Target::Module(uri.clone())),
2435 STeXAnnot::MathStructure { uri, .. } => {
2436 Some(Target::Structure(uri.uri.clone()))
2437 }
2438 STeXAnnot::MorphismEnv { uri, .. } | STeXAnnot::InlineMorphism { uri, .. } => {
2439 Some(Target::Morphism(uri.clone()))
2440 }
2441 STeXAnnot::Symdecl { uri, .. }
2442 | STeXAnnot::TextSymdecl { uri, .. }
2443 | STeXAnnot::Paragraph {
2444 symbol: Some(uri), ..
2445 }
2446 | STeXAnnot::InlineParagraph {
2447 symbol: Some(uri), ..
2448 }
2449 | STeXAnnot::Symdef { uri, .. } => Some(Target::Symbol(uri.uri.clone())),
2450 STeXAnnot::RenameDecl { .. } => None, STeXAnnot::Vardef { .. } | STeXAnnot::Varseq { .. } => {
2452 None
2454 }
2455 _ => None,
2456 })
2457 .await??;
2458 tokio::task::spawn_blocking(move || {
2459 let all = slf.documents.read();
2460 macro_rules! iter {
2461 ($annot:ident => $then:expr) => {
2462 for (url,data) in all.iter() {
2463 let data = match data {
2464 DocData::Data(d,_ ) => d,
2465 DocData::Doc(d) => &d.annotations
2466 };
2467 let data = data.lock();
2468 let iter : AnnotIter = data.annotations.iter().into();
2469 macro_rules! here {
2470 ($e:expr) => {
2471 lsp::Location {
2472 uri:url.clone().into(),
2473 range: SourceRange::into_range($e)
2474 }
2475 }
2476 }
2477 for $annot in <AnnotIter as TreeChildIter<STeXAnnot>>::dfs(iter) { $then }
2478 }
2479 }
2480 }
2481 let mut ret = Vec::new();
2482 match e {
2483 Target::Module(muri) => {
2484 iter!(a => match a {
2485 STeXAnnot::ImportModule{module,full_range,..} | STeXAnnot::UseModule{module,full_range,..} if module.uri == muri => {
2486 ret.push(here!(*full_range))
2487 }
2488 STeXAnnot::MorphismEnv{domain:ModuleOrStruct::Module(rf),domain_range,..} |
2489 STeXAnnot::InlineMorphism{domain:ModuleOrStruct::Module(rf),domain_range,..}
2490 if rf.uri == muri => ret.push(here!(*domain_range)),
2491 _ => ()
2492 })
2493 }
2494 Target::Structure(suri) | Target::Morphism(suri) | Target::Symbol(suri) => {
2495 iter!(a => match a {
2496 STeXAnnot::MathStructure{extends,..} => for (s,r) in extends {
2497 if s.uri == suri { ret.push(here!(*r)); }
2498 }
2499 STeXAnnot::ConservativeExt{uri,extstructure_range:range,..} |
2500 STeXAnnot::MorphismEnv{domain:ModuleOrStruct::Struct(uri),domain_range:range,..} |
2501 STeXAnnot::InlineMorphism{domain:ModuleOrStruct::Struct(uri),domain_range:range,..} |
2502 STeXAnnot::SemanticMacro{uri,token_range:range,..} |
2503 STeXAnnot::UseStructure{structure:uri,structure_range:range,..} |
2504 STeXAnnot::RenameDecl{uri,orig_range:range,..} |
2505 STeXAnnot::Assign{uri,orig_range:range,..}
2506 if uri.uri == suri => ret.push(here!(*range)),
2507 STeXAnnot::Notation{uri,name_range:range,..} |
2508 STeXAnnot::SymName{uri,name_range:range,..} |
2509 STeXAnnot::Symuse{uri,name_range:range,..} |
2510 STeXAnnot::Symref{uri,name_range:range,..} |
2511 STeXAnnot::Precondition{uri,symbol_range:range,.. } |
2512 STeXAnnot::Objective{uri,symbol_range:range,.. } |
2513 STeXAnnot::Definiens{uri,full_range:range,..} => {
2514 for u in uri {
2515 if u.uri == suri { ret.push(here!(*range)) }
2516 }
2517 }
2518 STeXAnnot::Paragraph{parsed_args,..} | STeXAnnot::InlineParagraph{parsed_args,..} => {
2519 for a in parsed_args {
2520 if let ParagraphArg::Fors(ParsedKeyValue{val,..}) = a {
2521 for (uri,range) in val {
2522 for u in uri {
2523 if u.uri == suri { ret.push(here!(*range)) }
2524 }
2525 }
2526 }
2527 }
2528 }
2529 _ => ()
2530 })
2531 }
2532 }
2533 ret
2534 }).await.ok()
2535 })
2536 }
2537
2538 #[must_use]
2539 pub fn get_hover(
2540 &self,
2541 uri: &UrlOrFile,
2542 position: lsp::Position,
2543 _: Option<ProgressCallbackClient>,
2544 ) -> Option<impl std::future::Future<Output = Option<lsp::Hover>> + use<>> {
2545 let d = self.get(uri)?;
2546 let da = d.archive().cloned();
2547 let pos = LSPLineCol {
2548 line: position.line,
2549 col: position.character,
2550 };
2551 Some(
2552 d.with_annots(self.clone(), move |data| {
2553 at_position(data, pos).and_then(|e| e.hover(da.as_ref(), pos))
2554 })
2555 .map(|o| o.flatten()),
2556 )
2557 }
2558
2559 #[must_use]
2560 pub fn get_codeaction(
2561 &self,
2562 uri: UrlOrFile,
2563 range: lsp::Range,
2564 _context: lsp::CodeActionContext,
2565 _: Option<ProgressCallbackClient>,
2566 ) -> Option<impl std::future::Future<Output = Option<lsp::CodeActionResponse>> + use<>> {
2567 let d = self.get(&uri)?;
2568 let pos = LSPLineCol {
2569 line: range.start.line,
2570 col: range.start.character,
2571 };
2572 let url = uri.into();
2573 Some(
2574 d.with_annots(self.clone(), move |data| {
2575 at_position(data, pos).map(|e| e.code_action(pos, &url))
2576 })
2577 .map(|o| o.flatten()),
2578 )
2579 }
2580
2581 #[must_use]
2582 pub fn get_goto_definition(
2583 &self,
2584 uri: UrlOrFile,
2585 position: lsp::Position,
2586 _: Option<ProgressCallbackClient>,
2587 ) -> Option<impl std::future::Future<Output = Option<lsp::GotoDefinitionResponse>> + use<>>
2588 {
2589 let d = self.get(&uri)?;
2590 let pos = LSPLineCol {
2591 line: position.line,
2592 col: position.character,
2593 };
2594 Some(
2595 d.with_annots(self.clone(), move |data| {
2596 at_position(data, pos).and_then(|e| e.goto_definition(&uri, pos))
2597 })
2598 .map(|o| o.flatten()),
2599 )
2600 }
2601
2602 #[must_use]
2603 pub fn get_inlay_hints(
2604 &self,
2605 uri: &UrlOrFile,
2606 _: Option<ProgressCallbackClient>,
2607 ) -> Option<impl std::future::Future<Output = Option<Vec<lsp::InlayHint>>> + use<>> {
2608 let d = self.get(uri)?;
2609 Some(d.with_annots(self.clone(), move |data| {
2610 let iter: AnnotIter = data.annotations.iter().into();
2611 <AnnotIter as TreeChildIter<STeXAnnot>>::dfs(iter)
2612 .filter_map(|e| e.inlay_hint())
2613 .collect()
2614 }))
2615 }
2616
2617 pub fn get_semantic_tokens(
2618 &self,
2619 uri: &UrlOrFile,
2620 progress: Option<ProgressCallbackClient>,
2621 _range: Option<lsp::Range>,
2622 ) -> Option<impl std::future::Future<Output = Option<lsp::SemanticTokens>> + use<>> {
2623 let d = self.get(uri)?;
2625 Some(d.with_annots(self.clone(), |data| {
2626 let mut ret = Vec::new();
2627 let mut curr = (0u32, 0u32);
2628 for e in data.annotations.iter() {
2629 e.semantic_tokens(&mut |range, tp| {
2630 if range.start.line < curr.0 {
2631 return;
2632 }
2633 let delta_line = range.start.line - curr.0;
2634 let delta_start = if delta_line == 0 {
2635 if range.start.col > curr.1 {
2636 range.start.col - curr.1
2637 } else {
2638 return;
2639 }
2640 } else {
2641 range.start.col
2642 };
2643 curr = (range.start.line, range.start.col);
2644 if range.start.line == range.end.line {
2645 let length = if range.end.col < range.start.col {
2646 999
2647 } else {
2648 range.end.col - range.start.col
2649 };
2650 ret.push(lsp::SemanticToken {
2651 delta_line,
2652 delta_start,
2653 length,
2654 token_type: tp,
2655 token_modifiers_bitset: 0,
2656 });
2657 } else {
2658 ret.push(lsp::SemanticToken {
2659 delta_line,
2660 delta_start,
2661 length: 999,
2662 token_type: tp,
2663 token_modifiers_bitset: 0,
2664 });
2665 }
2667 });
2668 }
2669
2670 if let Some(p) = progress {
2671 p.finish()
2672 }
2673 lsp::SemanticTokens {
2674 result_id: None,
2675 data: ret,
2676 }
2677 }))
2678 }
2679}
2680
2681fn at_position(data: &STeXParseDataI, position: LSPLineCol) -> Option<&STeXAnnot> {
2682 let mut ret = None;
2683 let iter: AnnotIter = data.annotations.iter().into();
2684 for e in <AnnotIter as TreeChildIter<STeXAnnot>>::dfs(iter) {
2685 let range = e.range();
2686 if range.contains(position) {
2687 ret = Some(e);
2688 } else if range.start > position {
2689 if ret.is_some() {
2690 break;
2691 }
2692 }
2693 }
2694 ret
2695}
2696
2697#[must_use]
2698pub fn to_diagnostic(diag: &STeXDiagnostic) -> lsp::Diagnostic {
2699 lsp::Diagnostic {
2700 range: diag.range.into_range(),
2701 severity: Some(match diag.level {
2702 DiagnosticLevel::Error => lsp::DiagnosticSeverity::ERROR,
2703 DiagnosticLevel::Info => lsp::DiagnosticSeverity::INFORMATION,
2704 DiagnosticLevel::Warning => lsp::DiagnosticSeverity::WARNING,
2705 DiagnosticLevel::Hint => lsp::DiagnosticSeverity::HINT,
2706 }),
2707 code: None,
2708 code_description: None,
2709 source: None,
2710 message: diag.message.clone(),
2711 related_information: None,
2712 tags: None,
2713 data: None,
2714 }
2715}