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