@@ -410,105 +410,6 @@ module Selection = {
410410 ~action= inject(Globals (Redo )),
411411 "Redo" ,
412412 ),
413- /* Navigation */
414- mk(
415- ~hotkey= "F12" ,
416- ~mdIcon= "arrow_forward" ,
417- ~section= "Navigation" ,
418- ~action=
419- inject(
420- Globals (
421- ActiveEditor (Move (Goal (BindingSiteOfIndicatedVar ))),
422- ),
423- ),
424- "Go to Definition" ,
425- ),
426- mk(
427- ~hotkey= "shift+tab" ,
428- ~mdIcon= "swipe_left_alt" ,
429- ~section= "Navigation" ,
430- ~action= inject(Globals (ActiveEditor (Move (Goal (Hole (Left )))))),
431- "Go to Previous Hole" ,
432- ),
433- mk(
434- ~mdIcon= "swipe_right_alt" ,
435- ~section= "Navigation" ,
436- ~action=
437- inject(Globals (ActiveEditor (Move (Goal (Hole (Right )))))),
438- "Go To Next Hole" ,
439- ),
440- /* Selection */
441- mk(
442- ~hotkey= meta ++ "+d" ,
443- ~mdIcon= "select_all" ,
444- ~section= "Selection" ,
445- ~action= inject(Globals (ActiveEditor (Select (Term (Current ))))),
446- "Select current term" ,
447- ),
448- mk(
449- ~mdIcon= "select_all" ,
450- ~hotkey= meta ++ "+a" ,
451- ~section= "Selection" ,
452- ~action= inject(Globals (ActiveEditor (Select (All )))),
453- "Select All" ,
454- ),
455- mk(
456- ~mdIcon= "flip_horizontal" ,
457- ~section= "Selection" ,
458- ~action= inject(Globals (ActiveEditor (Select (ToggleFocus )))),
459- "Toggle Selection Focus" ,
460- ),
461- mk(
462- ~mdIcon= "border_left" ,
463- ~section= "Selection" ,
464- ~hotkey= meta ++ "+alt+shift+left" ,
465- ~action= inject(Globals (ActiveEditor (Select (SetFocus (Left ))))),
466- "Set Selection Focus Left" ,
467- ),
468- mk(
469- ~mdIcon= "border_right" ,
470- ~section= "Selection" ,
471- ~hotkey= meta ++ "+alt+shift+right" ,
472- ~action= inject(Globals (ActiveEditor (Select (SetFocus (Right ))))),
473- "Set Selection Focus Right" ,
474- ),
475- /* Projection */
476- mk(
477- ~hotkey= "alt+f" ,
478- ~mdIcon= "camera" ,
479- ~section= "Projection" ,
480- ~action=
481- inject(
482- Globals (
483- ActiveEditor (Project (SetIndicated (Specific (Fold )))),
484- ),
485- ),
486- "Fold" ,
487- ),
488- mk(
489- ~hotkey= meta ++ "+e" ,
490- ~mdIcon= "camera" ,
491- ~section= "Projection" ,
492- ~action= inject(Globals (ActiveEditor (Probe (ToggleManual )))),
493- "Probe" ,
494- ),
495- mk(
496- ~hotkey= "alt+t" ,
497- ~mdIcon= "camera" ,
498- ~section= "Projection" ,
499- ~action= inject(Globals (ActiveEditor (Probe (ToggleStatics )))),
500- "Statics" ,
501- ),
502- mk(
503- ~hotkey= "alt+l" ,
504- ~mdIcon= "camera" ,
505- ~section= "Projection" ,
506- ~action=
507- inject(
508- Globals (ActiveEditor (Project (SetIndicated (ChooseLivelit )))),
509- ),
510- "Livelit" ,
511- ),
512413 /* Settings */
513414 mk(
514415 ~section= "Settings" ,
@@ -600,39 +501,20 @@ module Selection = {
600501 ~action= inject(Globals (Set (ExplainThis (ToggleShowFeedback )))),
601502 "Toggle Show Docs Feedback" ,
602503 ),
603- /* Editor tools */
604- mk(
605- ~hotkey= meta ++ "+/" ,
606- ~mdIcon= "assistant" ,
607- ~action= inject(Globals (ActiveEditor (Buffer (Set (TyDi ))))),
608- "TyDi Assistant" ,
609- ),
504+ /* Export / Diagnostics */
610505 mk(
611506 ~mdIcon= "download" ,
612507 ~section= "Export" ,
613508 ~action= inject(Globals (ExportForInit )),
614509 "Export For Init" ,
615510 ),
616- mk(
617- ~section= "Diagnostics" ,
618- ~mdIcon= "refresh" ,
619- ~action= inject(Globals (ActiveEditor (Reparse ))),
620- "Reparse Current Editor" ,
621- ),
622511 mk(
623512 ~mdIcon= "timer" ,
624513 ~section= "Diagnostics" ,
625514 ~hotkey= "F7" ,
626515 ~action= inject(Benchmark (Start )),
627516 "Run Benchmark" ,
628517 ),
629- mk(
630- ~mdIcon= "bolt" ,
631- ~section= "Refactoring" ,
632- ~hotkey= meta ++ "+i" ,
633- ~action= inject(Globals (ActiveEditor (Introduce ))),
634- "Introduce" ,
635- ),
636518 ] );
637519 };
638520};
@@ -799,7 +681,10 @@ module View = {
799681 Effect . Ignore ;
800682 } else {
801683 copy(cursor);
802- inject(Globals (ActiveEditor (Destruct (Right ))));
684+ switch (cursor. editor_action(Destruct (Right ))) {
685+ | Some (action ) => inject(Editors (action))
686+ | None => Effect . Ignore
687+ };
803688 };
804689 | None => Effect . Ignore
805690 };
0 commit comments