<commit_before>import { basename, escapeHtml, colorizeMessage } from './util';
import { Message } from 'lean-client-js-node';
import * as React from 'react';
import { Location, Config } from '../src/shared';
import { CopyToCommentIcon } from './svg_icons';

function compareMessages(m1: Message, m2: Message): boolean {
    return (m1.file_name === m2.file_name &&
        m1.pos_line === m2.pos_line && m1.pos_col === m2.pos_col &&
        m1.severity === m2.severity && m1.caption === m2.caption && m1.text === m2.text);
}

interface MessageViewProps {
    m: Message;
    onCopyToComment?: (x: string) => void;
}

export function MessageView(props: MessageViewProps) {
    const {m, onCopyToComment} = props;
    const b = escapeHtml(basename(m.file_name));
    const l = m.pos_line; const c = m.pos_col;
    const shouldColorize = m.severity === 'error';
    let text = escapeHtml(m.text)
    text = shouldColorize ? colorizeMessage(text) : text;
    const title = `${b}:${l}:${c}`;
    return <details open>
        <summary className={m.severity + ' mv2 pointer'}>{title}
            {onCopyToComment &&
                <span className="fr">
                    <a className="link pointer mh3 dim" title="copy message to comment" onClick={e => {e.preventDefault(); onCopyToComment(m.text)}}><CopyToCommentIcon/></a>
                </span>
            }
        </summary>
        <div className="ml1">
            <pre className="font-code" style={{whiteSpace: 'pre-wrap'}} dangerouslySetInnerHTML={{ __html: text }} />
        </div>
    </details>
}

interface MessagesProps {
    messages: (Message & {key?})[];
    onCopyToComment?: (text: string) => void;
}

export function Messages(props: MessagesProps): JSX.Element {
    const should_hide = !props.messages || props.messages.length === 0;
    if (should_hide) {return <>No messages.</>}
    const msgs = (props.messages || []).map((m,i) =><commit_msg>Add reveal button to messages.<commit_after>import { basename, escapeHtml, colorizeMessage } from './util';
import { Message } from 'lean-client-js-node';
import * as React from 'react';
import { Location, Config } from '../src/shared';
import { CopyToCommentIcon, GoToFileIcon } from './svg_icons';
import { post } from './server';

function compareMessages(m1: Message, m2: Message): boolean {
    return (m1.file_name === m2.file_name &&
        m1.pos_line === m2.pos_line && m1.pos_col === m2.pos_col &&
        m1.severity === m2.severity && m1.caption === m2.caption && m1.text === m2.text);
}

interface MessageViewProps {
    m: Message;
    onCopyToComment?: (x: string) => void;
}

export function MessageView(props: MessageViewProps) {
    const {m, onCopyToComment} = props;
    const b = escapeHtml(basename(m.file_name));
    const l = m.pos_line; const c = m.pos_col;
    const loc: Location = {file_name: m.file_name, column: c, line: l}
    const shouldColorize = m.severity === 'error';
    let text = escapeHtml(m.text)
    text = shouldColorize ? colorizeMessage(text) : text;
    const title = `${b}:${l}:${c}`;
    return <details open>
        <summary className={m.severity + ' mv2 pointer'}>{title}
            {onCopyToComment &&
                <span className="fr">
                    <a className={'link pointer mh2 dim '} onClick={e => { e.preventDefault(); post({command: 'reveal', loc}); }} title="reveal file location"><GoToFileIcon/></a>
                    <a className="link pointer mh2 dim" title="copy message to comment" onClick={e => {e.preventDefault(); onCopyToComment(m.text)}}><CopyToCommentIcon/></a>
                </span>
            }
        </summary>
        <div className="ml1">
            <pre className="font-code" style={{whiteSpace: 'pre-wrap'}} dangerouslySetInnerHTML={{ __html: text }} />
        </div>
    </details>
}

interface MessagesProps {
    messages: (Message & {key?})[];
    onCopyToComment?: (text: string) => void;
}

export function Messages(props: MessagesProps): JSX.Element {
    const should_hide = !props.messages || props.messages.length === 0;
    if (should_hide) {return <>No messages.</>}
    const msgs = (props.messages || []).map((m,i) =>
{'fraction_non_alphanumeric': 0.1632111861137898, 'fraction_numerical': 0.008919961427193828, 'mean_word_length': 3.216463414634146, 'pattern_counts': {'":': 0, '<': 34, '<?xml version=': 0, '>': 43, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5485156', 'n_tokens_mistral': 1313, 'n_tokens_neox': 1305, 'n_words': 321}