Type Alias HighlightedMsgEmbed

HighlightedMsgEmbed:
    | { expr: HighlightedCodeWithInfos }
    | { goal: InteractiveGoal }
    | {
        widget: {
            alt: TaggedText<HighlightedMsgEmbed>;
            wi: UserWidgetInstance;
        };
    }
    | { trace: HighlightedTraceEmbed }
    | "highlighted"