/* ============================================================
   Lambda Calculus Explorer — Stylesheet
   CIS352 at Syracuse University
   light theme, glassmorphism, JetBrains Mono, Syracuse Orange
   ============================================================ */

/* --- Brand Palette (Syracuse University official) --- */
:root {
    --brand:        #F76900;   /* Syracuse Orange (official PMS 158 C) */
    --brand-dark:   #D74100;   /* hover / pressed (official dark orange) */
    --brand-mid:    #FF8E00;   /* lighter accent (official light orange) */
    --brand-soft:   #FFB366;   /* muted orange */
    --brand-pale:   #FDDCB5;   /* very light border */
    --brand-wash:   #FFF2E5;   /* light background */
    --brand-tint:   #FFFAF5;   /* whisper background */

    /* Semantic — Syracuse Navy for beta, Syracuse Blue for alpha/binding */
    --sem-beta:     #000E54;   /* Syracuse Navy (official PMS 281 C) — beta reduction */
    --sem-alpha:    #2B72D7;   /* Syracuse Light Blue — alpha conversion */
    --sem-eta:      #059669;   /* green — eta conversion */
    --sem-bound:    #0d9488;   /* teal — bound variables */
    --sem-free:     #FF431B;   /* Syracuse Medium Orange — free variables */
    --sem-binding:  #2B72D7;   /* Syracuse Light Blue — binding site */
    --sem-result:   #f59e0b;   /* amber — reduction highlight */
}

/* --- Reset & Base --- */
*, *::before, *::after { margin: 0; padding: 0; box-sizing: border-box; }
html, body { height: 100%; overflow: hidden; overscroll-behavior: none; }

body {
    font-family: 'Inter', -apple-system, BlinkMacSystemFont, 'Segoe UI', sans-serif;
    background: #fafafa;
    color: #374151;
    -webkit-font-smoothing: antialiased;
}

#app {
    height: 100%;
    display: flex;
    flex-direction: column;
}

/* --- Back to CIS352 Bar --- */
.back-bar {
    position: fixed;
    top: 0;
    right: 0;
    display: inline-flex;
    align-items: center;
    gap: 6px;
    padding: 6px 18px 7px 12px;
    font-family: 'Inter', sans-serif;
    font-size: 0.82em;
    font-weight: 600;
    color: rgba(247, 105, 0, 0.6);
    text-decoration: none;
    background: rgba(247, 105, 0, 0.025);
    border-bottom-left-radius: 8px;
    border-left: 1px solid rgba(247, 105, 0, 0.06);
    border-bottom: 1px solid rgba(247, 105, 0, 0.06);
    box-shadow:
        inset 0 1px 4px rgba(0, 0, 0, 0.04),
        inset 1px 0 3px rgba(0, 0, 0, 0.02);
    z-index: 90;
    transition: color 0.3s, background 0.3s;
    cursor: pointer;
    user-select: none;
    letter-spacing: 0.01em;
}

.back-bar:hover {
    color: rgba(247, 105, 0, 0.75);
    background: rgba(247, 105, 0, 0.05);
}

.back-bar .back-arrow {
    font-size: 0.9em;
    opacity: 0.5;
    transition: opacity 0.2s, transform 0.2s;
}

.back-bar:hover .back-arrow {
    opacity: 0.8;
    transform: translateX(-2px);
}

.back-bar .back-text strong {
    font-weight: 700;
    color: rgba(247, 105, 0, 0.7);
    transition: color 0.3s;
}

.back-bar:hover .back-text strong {
    color: rgba(247, 105, 0, 0.9);
}

/* --- Floating Input Bar --- */
#input-bar {
    position: fixed;
    bottom: 12px;
    left: 50%;
    transform: translateX(-50%);
    display: flex;
    align-items: center;
    gap: 10px;
    padding: 6px 10px 6px 14px;
    background: rgba(255, 255, 255, 0.92);
    backdrop-filter: blur(20px);
    -webkit-backdrop-filter: blur(20px);
    border: 1px solid rgba(0, 0, 0, 0.07);
    border-radius: 14px;
    box-shadow: 0 -2px 20px rgba(0, 0, 0, 0.06), 0 0 0 1px rgba(0,0,0,0.02);
    z-index: 100;
    max-width: calc(100vw - 32px);
    transition: box-shadow 0.2s;
}

#input-bar:focus-within {
    box-shadow: 0 -2px 28px rgba(247, 105, 0, 0.08), 0 0 0 1px rgba(247, 105, 0, 0.10);
}

.logo {
    font-family: 'JetBrains Mono', 'SF Mono', 'Menlo', monospace;
    font-size: 22px;
    font-weight: 700;
    color: var(--brand);
    line-height: 1;
    flex-shrink: 0;
}

/* --- Drawer FAB --- */
.drawer-fab {
    position: fixed;
    top: 14px;
    left: 14px;
    width: 40px;
    height: 40px;
    border-radius: 12px;
    border: 1px solid rgba(0, 0, 0, 0.07);
    background: rgba(255, 255, 255, 0.88);
    backdrop-filter: blur(16px);
    -webkit-backdrop-filter: blur(16px);
    box-shadow: 0 2px 16px rgba(0, 0, 0, 0.06);
    cursor: pointer;
    display: flex;
    align-items: center;
    justify-content: center;
    z-index: 110;
    color: #6b7280;
    transition: all 0.2s cubic-bezier(0.4, 0, 0.2, 1);
}

.drawer-fab:hover {
    background: rgba(255, 255, 255, 0.96);
    color: var(--brand);
    box-shadow: 0 4px 20px rgba(247, 105, 0, 0.10);
    border-color: rgba(247, 105, 0, 0.16);
}

.drawer-fab:active {
    transform: scale(0.94);
}

/* --- Drawer Backdrop --- */
.drawer-backdrop {
    position: fixed;
    inset: 0;
    background: rgba(0, 0, 0, 0.08);
    backdrop-filter: blur(2px);
    -webkit-backdrop-filter: blur(2px);
    z-index: 119;
    opacity: 0;
    pointer-events: none;
    transition: opacity 0.3s cubic-bezier(0.4, 0, 0.2, 1);
}

.drawer-backdrop.visible {
    opacity: 1;
    pointer-events: auto;
}

/* --- Side Drawer --- */
.drawer {
    position: fixed;
    top: 0;
    left: 0;
    bottom: 0;
    width: 280px;
    background: rgba(255, 255, 255, 0.94);
    backdrop-filter: blur(24px);
    -webkit-backdrop-filter: blur(24px);
    border-right: 1px solid rgba(0, 0, 0, 0.06);
    box-shadow: 8px 0 40px rgba(0, 0, 0, 0.06);
    z-index: 120;
    display: flex;
    flex-direction: column;
    transform: translateX(-100%);
    transition: transform 0.3s cubic-bezier(0.4, 0, 0.2, 1);
    overflow: hidden;
}

.drawer.open {
    transform: translateX(0);
}

.drawer-header {
    display: flex;
    align-items: flex-start;
    justify-content: space-between;
    padding: 18px 18px 14px;
    border-bottom: 1px solid rgba(0, 0, 0, 0.05);
    flex-wrap: wrap;
}

.drawer-title {
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.88em;
    font-weight: 600;
    color: var(--brand);
    letter-spacing: -0.01em;
}

.drawer-subtitle {
    display: block;
    width: 100%;
    font-family: 'Inter', sans-serif;
    font-size: 0.68em;
    font-weight: 400;
    color: #9ca3af;
    letter-spacing: 0.04em;
    margin-top: 2px;
    order: 3;
}

.drawer-close-btn {
    width: 28px;
    height: 28px;
    border-radius: 8px;
    border: none;
    background: transparent;
    color: #9ca3af;
    font-size: 1.3em;
    cursor: pointer;
    display: flex;
    align-items: center;
    justify-content: center;
    transition: all 0.15s;
}

.drawer-close-btn:hover {
    background: rgba(0, 0, 0, 0.05);
    color: #374151;
}

.drawer-body {
    flex: 1;
    overflow-y: auto;
    padding: 6px 0;
}

.drawer-section {
    padding: 12px 18px;
}

.drawer-section + .drawer-section {
    border-top: 1px solid rgba(0, 0, 0, 0.04);
}

.drawer-section-label {
    font-size: 0.68em;
    font-weight: 600;
    text-transform: uppercase;
    letter-spacing: 0.06em;
    color: #9ca3af;
    margin-bottom: 10px;
}

.drawer-actions {
    display: flex;
    flex-direction: column;
    gap: 8px;
}

.drawer-row {
    display: flex;
    align-items: center;
    gap: 8px;
}

.drawer-info-row {
    display: flex;
    align-items: center;
    gap: 10px;
    margin-top: 10px;
}

.drawer-info {
    font-size: 0.78em;
    color: #6b7280;
}

.btn-flex {
    flex: 1;
}

.btn-wide {
    width: 100%;
}

.btn-wide kbd, .btn-flex kbd {
    margin-left: auto;
    opacity: 0.5;
    font-size: 0.85em;
}

.input-group {
    display: flex;
    flex: 1;
    min-width: 200px;
    max-width: 420px;
}

.input-group input {
    flex: 1;
    height: 34px;
    padding: 0 10px;
    border: 1px solid #d1d5db;
    border-right: none;
    border-radius: 8px 0 0 8px;
    font-family: 'JetBrains Mono', 'SF Mono', 'Menlo', monospace;
    font-size: 0.82em;
    color: #374151;
    background: #fff;
    outline: none;
    transition: border-color 0.15s;
}

.input-group input:focus {
    border-color: var(--brand);
}

.input-group .btn {
    border-radius: 0 8px 8px 0;
}

/* --- Buttons --- */
.btn {
    height: 34px;
    padding: 0 14px;
    border: 1px solid #d1d5db;
    border-radius: 6px;
    background: #fff;
    color: #374151;
    font-family: inherit;
    font-size: 0.82em;
    font-weight: 500;
    cursor: pointer;
    transition: all 0.15s;
    white-space: nowrap;
    display: inline-flex;
    align-items: center;
    justify-content: center;
}

.btn:hover {
    background: #f3f4f6;
    border-color: #9ca3af;
}

.btn:active {
    background: #e5e7eb;
}

.btn:disabled {
    opacity: 0.4;
    cursor: default;
    pointer-events: none;
}

.btn-primary {
    background: var(--brand);
    color: #fff;
    border-color: var(--brand);
}

.btn-primary:hover {
    background: var(--brand-dark);
    border-color: var(--brand-dark);
}

.btn-icon {
    width: 34px;
    padding: 0;
    font-size: 1em;
}

.btn-small {
    font-size: 0.72em;
    width: auto;
    padding: 0 8px;
}

.select {
    height: 34px;
    padding: 0 8px;
    border: 1px solid #d1d5db;
    border-radius: 6px;
    background: #fff;
    color: #374151;
    font-family: inherit;
    font-size: 0.82em;
    cursor: pointer;
    outline: none;
}

.select:focus {
    border-color: var(--brand);
}

.checkbox-label {
    display: flex;
    align-items: center;
    gap: 4px;
    font-size: 0.82em;
    color: #6b7280;
    cursor: pointer;
    white-space: nowrap;
}

/* Strategy grid in drawer */
.strategy-grid {
    display: grid;
    grid-template-columns: 1fr 1fr;
    gap: 6px;
}

.strategy-btn {
    padding: 0 10px;
    gap: 6px;
    font-size: 0.78em;
    border-radius: 8px;
    justify-content: space-between;
}

.strategy-btn kbd {
    display: inline-flex;
    align-items: center;
    justify-content: center;
    width: 18px;
    height: 18px;
    border: 1px solid #d1d5db;
    border-radius: 4px;
    background: #f3f4f6;
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.8em;
    font-weight: 600;
    color: #9ca3af;
    line-height: 1;
}

.strategy-btn.active {
    background: var(--brand-tint);
    border-color: var(--brand-soft);
    color: var(--brand);
    font-weight: 600;
}

.strategy-btn.active kbd {
    background: var(--brand-wash);
    border-color: var(--brand-pale);
    color: var(--brand);
}

.zoom-controls {
    display: flex;
    align-items: center;
    gap: 4px;
}

.zoom-label {
    font-size: 0.75em;
    font-weight: 500;
    color: #9ca3af;
    min-width: 40px;
    text-align: center;
}

/* --- Viewport --- */
#viewport {
    flex: 1;
    overflow: hidden;
    cursor: grab;
    position: relative;
}

#viewport.dragging {
    cursor: grabbing;
}

#term-container {
    transform-origin: 0 0;
    transition: none;
}

#term-display {
    position: relative;
    user-select: none;
    -webkit-user-select: none;
}

/* --- Main Tree View --- */
.main-edges {
    position: absolute;
    top: 0;
    left: 0;
    pointer-events: none;
    overflow: visible;
}

.main-edge-label {
    font-family: 'JetBrains Mono', monospace;
    font-size: 13px;
    font-weight: 700;
    fill: var(--brand-pale);
}

.main-edge-label.active {
    fill: var(--brand-soft);
}

.main-node-card {
    position: absolute;
    transform: translateX(-50%);
    font-family: 'JetBrains Mono', 'SF Mono', 'Menlo', 'Consolas', monospace;
    font-size: 20px;
    line-height: 1.7;
    white-space: nowrap;
    cursor: pointer;
    transition: opacity 0.3s, box-shadow 0.3s;
    user-select: none;
    padding: 4px 8px;
    border-radius: 6px;
}

.main-node-card.current {
    cursor: default;
    background: rgba(247, 105, 0, 0.03);
    box-shadow: 0 0 0 1.5px rgba(247, 105, 0, 0.12), 0 1px 8px rgba(247, 105, 0, 0.05);
}

.main-node-card.on-path {
    opacity: 0.75;
}

.main-node-card.off-path {
    opacity: 0.45;
}

.main-node-card.off-path:hover {
    opacity: 0.7;
}

.main-node-card.on-path:hover {
    opacity: 0.95;
}

/* Church-Rosser demo: make all branches visible */
.show-all-branches .main-node-card.off-path {
    opacity: 0.85;
}

.show-all-branches .main-edge-label {
    fill: var(--brand-soft);
}

/* --- Empty State --- */
#empty-state {
    display: flex;
    flex-direction: column;
    align-items: center;
    gap: 12px;
    color: #9ca3af;
    pointer-events: none;
}

.empty-icon {
    font-family: 'JetBrains Mono', monospace;
    font-size: 64px;
    font-weight: 700;
    color: #e5e7eb;
    line-height: 1;
}

#empty-state p {
    font-size: 0.9em;
}

/* --- Term Rendering --- */
.term {
    display: inline;
    position: relative;
    border-radius: 3px;
    transition: background 0.12s, box-shadow 0.12s;
    padding: 1px 0;
}

/* Non-actionable terms: no pointer, no highlight */
.term:not(.has-op) {
    cursor: default;
}

.term.has-op {
    cursor: pointer;
}

/* ONLY highlight terms with operations */
.term.has-op.hovered {
    background: rgba(247, 105, 0, 0.06);
    box-shadow: 0 0 0 2px rgba(247, 105, 0, 0.14);
}

.term.strategy-next {
    background: rgba(247, 105, 0, 0.03);
}

.term.strategy-next.hovered {
    background: rgba(247, 105, 0, 0.08);
}

/* Syntax tokens */
.lambda-sym {
    color: var(--brand);
    font-weight: 600;
}

.paren {
    color: #9ca3af;
}

.var-binding {
    color: var(--sem-binding);
    font-weight: 500;
}

.var-ref {
    color: var(--sem-bound);
    transition: color 0.12s, text-shadow 0.12s;
}

.var-ref.free {
    color: var(--sem-free);
    font-style: italic;
}

.var-ref.binding-highlight {
    text-shadow: 0 0 8px rgba(43, 114, 215, 0.3);
    color: var(--sem-binding);
}

.var-binding.binding-highlight {
    text-shadow: 0 0 8px rgba(43, 114, 215, 0.3);
}

/* Binding arrow overlay */
.binding-arrow-overlay {
    animation: binding-arrow-fadein 0.25s ease-out;
}

.binding-arrow-path {
    stroke-dasharray: 200;
    stroke-dashoffset: 200;
    animation: binding-arrow-draw 0.4s cubic-bezier(0.4, 0, 0.2, 1) forwards;
}

@keyframes binding-arrow-fadein {
    from { opacity: 0; }
    to { opacity: 1; }
}

@keyframes binding-arrow-draw {
    to { stroke-dashoffset: 0; }
}

/* Redex styling */
.term-app.redex > .paren {
    color: var(--sem-beta);
}

.term-app.redex.hovered {
    background: rgba(0, 14, 84, 0.08);
    box-shadow: 0 0 0 2px rgba(0, 14, 84, 0.20);
}

/* Eta styling */
.term-abs.eta-convertible.hovered {
    background: rgba(5, 150, 105, 0.08);
    box-shadow: 0 0 0 2px rgba(5, 150, 105, 0.20);
}

/* Pretty-print indentation */
.pp-indent {
    display: inline-block;
}

/* Redex highlight — shows which subterm was reduced in parent */
.term.redex-highlight {
    background: rgba(245, 158, 11, 0.14);
    box-shadow: 0 0 0 2px rgba(245, 158, 11, 0.28);
    border-radius: 3px;
}

/* Reduction result — matching highlight in current term */
.term.reduction-result {
    background: rgba(245, 158, 11, 0.14);
    box-shadow: 0 0 0 2px rgba(245, 158, 11, 0.28);
    border-radius: 3px;
}

/* Hold-B: highlight all beta redexes */
.show-redexes .term-app.redex {
    background: rgba(0, 14, 84, 0.10);
    box-shadow: 0 0 0 2px rgba(0, 14, 84, 0.22);
    border-radius: 3px;
}

.show-redexes .term-app.redex > .paren {
    color: var(--sem-beta);
}

/* Strategy tutorial: show all redexes with subtle outline, strategy-selected one in green */
.show-strategy-redexes .term-app.redex {
    background: rgba(0, 14, 84, 0.03);
    box-shadow: 0 0 0 1.5px rgba(0, 14, 84, 0.12);
    border-radius: 3px;
    transition: background 0.3s, box-shadow 0.3s;
}

.show-strategy-redexes .term-app.redex > .paren {
    color: rgba(0, 14, 84, 0.35);
}

.show-strategy-redexes .term-app.redex.strategy-next {
    background: rgba(5, 150, 105, 0.12);
    box-shadow: 0 0 0 2.5px rgba(5, 150, 105, 0.45);
}

.show-strategy-redexes .term-app.redex.strategy-next > .paren {
    color: var(--sem-eta);
}

/* Fade-in animation for newly rendered terms */
@keyframes term-fadein {
    from { opacity: 0; transform: translateY(4px); }
    to { opacity: 1; transform: translateY(0); }
}

.term-animate {
    animation: term-fadein 0.3s ease-out;
}

/* --- Context Menu: compact floating circles --- */
#context-menu {
    position: fixed;
    display: flex;
    gap: 6px;
    padding: 6px 8px;
    border-radius: 24px;
    background: rgba(255, 255, 255, 0.97);
    backdrop-filter: blur(16px);
    -webkit-backdrop-filter: blur(16px);
    border: 1px solid rgba(0, 0, 0, 0.06);
    box-shadow: 0 4px 24px rgba(0, 0, 0, 0.12), 0 0 0 1px rgba(0,0,0,0.02);
    z-index: 200;
    min-width: 0;
}

#context-menu.hidden {
    display: none;
}

.ctx-btn {
    width: 40px;
    height: 40px;
    border-radius: 50%;
    border: none;
    font-family: 'JetBrains Mono', 'SF Mono', monospace;
    font-size: 1.15em;
    font-weight: 600;
    cursor: pointer;
    transition: all 0.15s cubic-bezier(0.4, 0, 0.2, 1);
    display: flex;
    align-items: center;
    justify-content: center;
}

.ctx-btn:hover {
    transform: scale(1.12);
}

.ctx-btn:active {
    transform: scale(0.96);
}

.ctx-btn.beta {
    background: rgba(0, 14, 84, 0.10);
    color: var(--sem-beta);
}

.ctx-btn.beta:hover {
    background: rgba(0, 14, 84, 0.18);
    box-shadow: 0 0 16px rgba(0, 14, 84, 0.20);
}

.ctx-btn.alpha {
    background: rgba(43, 114, 215, 0.10);
    color: var(--sem-alpha);
}

.ctx-btn.alpha:hover {
    background: rgba(43, 114, 215, 0.18);
    box-shadow: 0 0 16px rgba(43, 114, 215, 0.20);
}

.ctx-btn.eta {
    background: rgba(5, 150, 105, 0.10);
    color: var(--sem-eta);
}

.ctx-btn.eta:hover {
    background: rgba(5, 150, 105, 0.18);
    box-shadow: 0 0 16px rgba(5, 150, 105, 0.20);
}

/* --- Inline Alpha Rename Popup --- */
.alpha-popup {
    position: fixed;
    display: flex;
    align-items: center;
    gap: 6px;
    padding: 5px 10px;
    background: rgba(255, 255, 255, 0.97);
    backdrop-filter: blur(16px);
    -webkit-backdrop-filter: blur(16px);
    border: 1px solid rgba(43, 114, 215, 0.18);
    border-radius: 10px;
    box-shadow: 0 4px 24px rgba(0, 0, 0, 0.10), 0 0 0 1px rgba(0,0,0,0.02);
    z-index: 300;
    font-family: 'JetBrains Mono', monospace;
}

.alpha-popup.hidden {
    display: none;
}

.alpha-tag {
    font-size: 0.8em;
    font-weight: 700;
    color: var(--sem-alpha);
    opacity: 0.5;
}

.alpha-old {
    font-size: 0.95em;
    font-weight: 600;
    color: var(--sem-alpha);
}

.alpha-arrow {
    font-size: 0.9em;
    color: #9ca3af;
}

.alpha-input {
    width: 64px;
    height: 28px;
    padding: 0 8px;
    border: 1.5px solid #e5e7eb;
    border-radius: 6px;
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.9em;
    color: #374151;
    background: #fff;
    outline: none;
    transition: border-color 0.15s, box-shadow 0.15s;
}

.alpha-input:focus {
    border-color: var(--brand);
    box-shadow: 0 0 0 2px rgba(247, 105, 0, 0.08);
}

/* (Strategy controls in side drawer) */

.badge {
    display: inline-flex;
    align-items: center;
    padding: 2px 8px;
    border-radius: 4px;
    font-size: 0.78em;
    font-weight: 600;
}

.badge-green {
    background: #ecfdf5;
    color: #065f46;
    border: 1px solid #a7f3d0;
}


/* --- Derivation Tree Panel --- */
#tree-panel {
    position: fixed;
    bottom: 36px;
    left: 16px;
    max-width: 360px;
    max-height: 280px;
    background: rgba(255, 255, 255, 0.95);
    backdrop-filter: blur(12px);
    -webkit-backdrop-filter: blur(12px);
    border: 1px solid rgba(0, 0, 0, 0.08);
    border-radius: 12px;
    box-shadow: 0 4px 24px rgba(0, 0, 0, 0.08);
    z-index: 90;
    overflow: hidden;
    display: flex;
    flex-direction: column;
    transition: opacity 0.2s, transform 0.2s;
}

#tree-panel.hidden {
    display: none;
}

#tree-panel.collapsed {
    max-height: 36px;
}

.tree-panel-header {
    display: flex;
    align-items: center;
    justify-content: space-between;
    padding: 8px 12px;
    border-bottom: 1px solid rgba(0, 0, 0, 0.04);
    flex-shrink: 0;
    cursor: pointer;
}

.tree-panel-header span {
    font-size: 0.75em;
    font-weight: 600;
    color: #6b7280;
    text-transform: uppercase;
    letter-spacing: 0.04em;
}

#tree-view {
    padding: 8px 8px 8px 4px;
    overflow-y: auto;
    overflow-x: auto;
    flex: 1;
}

/* Tree nodes */
.dtree-node {
    /* no extra padding on root */
}

.dtree-label {
    display: flex;
    align-items: center;
    gap: 6px;
    padding: 3px 8px;
    border-radius: 6px;
    cursor: pointer;
    transition: background 0.1s;
}

.dtree-label:hover {
    background: rgba(247, 105, 0, 0.05);
}

.dtree-label.current {
    background: rgba(247, 105, 0, 0.07);
}

.dtree-dot {
    width: 7px;
    height: 7px;
    border-radius: 50%;
    background: #d1d5db;
    flex-shrink: 0;
    transition: background 0.15s;
}

.dtree-label.current .dtree-dot {
    background: var(--brand);
    box-shadow: 0 0 6px rgba(247, 105, 0, 0.25);
}

.dtree-dot.diamond {
    border-radius: 2px;
    transform: rotate(45deg);
    background: var(--brand-mid);
}

.dtree-label.current .dtree-dot.diamond {
    background: var(--brand);
}

.dtree-ref {
    font-size: 0.7em;
    color: var(--brand-pale);
    margin-left: 4px;
}

.dtree-text {
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.68em;
    color: #9ca3af;
    overflow: hidden;
    text-overflow: ellipsis;
    white-space: nowrap;
    max-width: 280px;
}

.dtree-label.current .dtree-text {
    color: #374151;
    font-weight: 500;
}

.dtree-self-loop {
    display: flex;
    align-items: center;
    gap: 5px;
    margin-left: 14px;
    padding: 3px 8px;
    border-radius: 6px;
    cursor: pointer;
    transition: background 0.1s;
    border: 1px dashed rgba(247, 105, 0, 0.25);
    background: rgba(247, 105, 0, 0.03);
    margin-top: 2px;
}

.dtree-self-loop:hover {
    background: rgba(247, 105, 0, 0.07);
}

.dtree-loop-arrow {
    font-size: 1em;
    color: var(--brand);
    animation: loop-spin 2s linear infinite;
}

@keyframes loop-spin {
    from { transform: rotate(0deg); }
    to { transform: rotate(-360deg); }
}

.dtree-loop-label {
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.65em;
    color: rgba(247, 105, 0, 0.6);
    font-weight: 500;
}

.dtree-children {
    margin-left: 11px;
    border-left: 1.5px solid #e5e7eb;
    padding-left: 0;
}

.dtree-branch {
    display: flex;
    align-items: flex-start;
    gap: 0;
}

.dtree-edge {
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.62em;
    font-weight: 600;
    color: var(--brand-pale);
    padding: 4px 4px 0 2px;
    flex-shrink: 0;
    min-width: 16px;
    text-align: center;
}

/* --- Tutorial Tree Callout --- */
.tree-callout {
    position: fixed;
    bottom: 190px;
    left: 24px;
    z-index: 145;
    display: flex;
    flex-direction: column;
    align-items: flex-start;
    pointer-events: none;
    animation: callout-fadein 0.6s cubic-bezier(0.22, 1, 0.36, 1) both;
}

.tree-callout.hidden {
    display: none;
}

.tree-callout-svg {
    width: 140px;
    height: 100px;
    overflow: visible;
    filter: drop-shadow(0 1px 2px rgba(0, 0, 0, 0.06));
}

.tree-callout-stroke,
.tree-callout-head {
    stroke: rgba(120, 80, 40, 0.5);
    stroke-dasharray: 300;
    stroke-dashoffset: 300;
    animation: callout-draw 1.2s cubic-bezier(0.4, 0, 0.2, 1) 0.3s forwards;
}

.tree-callout-text {
    font-family: 'Georgia', 'Times New Roman', serif;
    font-style: italic;
    font-size: 0.82em;
    color: rgba(120, 80, 40, 0.6);
    margin-left: 90px;
    margin-top: -6px;
    letter-spacing: 0.01em;
    text-shadow: 0 1px 0 rgba(255, 255, 255, 0.8);
    opacity: 0;
    animation: callout-textfade 0.5s ease 1.2s forwards;
}

@keyframes callout-draw {
    to { stroke-dashoffset: 0; }
}

@keyframes callout-textfade {
    to { opacity: 1; }
}

@keyframes callout-fadein {
    from { opacity: 0; transform: translateY(8px); }
    to { opacity: 1; transform: translateY(0); }
}

/* --- Drawer Shortcuts --- */
.drawer-shortcuts {
    margin-top: auto;
}

.shortcut-grid {
    display: flex;
    flex-direction: column;
    gap: 6px;
}

.shortcut-row {
    display: flex;
    align-items: center;
    gap: 8px;
    font-size: 0.75em;
    color: #6b7280;
}

.shortcut-row kbd {
    display: inline-flex;
    align-items: center;
    justify-content: center;
    min-width: 24px;
    height: 22px;
    padding: 0 6px;
    border: 1px solid #e5e7eb;
    border-radius: 5px;
    background: #f9fafb;
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.85em;
    font-weight: 600;
    color: #6b7280;
    box-shadow: 0 1px 0 #e5e7eb;
    line-height: 1;
}

/* --- Tutorial FAB --- */
.tutorial-fab {
    position: fixed;
    top: 38px;
    right: 14px;
    width: 40px;
    height: 40px;
    border-radius: 50%;
    border: 2px solid var(--brand-soft);
    background: linear-gradient(135deg, var(--brand-tint) 0%, var(--brand-wash) 100%);
    cursor: pointer;
    display: flex;
    align-items: center;
    justify-content: center;
    z-index: 110;
    transition: all 0.2s cubic-bezier(0.4, 0, 0.2, 1);
    box-shadow: 0 2px 12px rgba(247, 105, 0, 0.14);
    animation: tut-fab-pulse 2s ease-in-out infinite;
}

.tutorial-fab:hover {
    transform: scale(1.1);
    box-shadow: 0 4px 20px rgba(247, 105, 0, 0.25);
    border-color: var(--brand);
}

.tutorial-fab:active {
    transform: scale(0.95);
}

.tutorial-fab-icon {
    font-family: 'Inter', sans-serif;
    font-size: 18px;
    font-weight: 700;
    color: var(--brand);
    line-height: 1;
}

@keyframes tut-fab-pulse {
    0%, 100% { box-shadow: 0 2px 12px rgba(247, 105, 0, 0.14); }
    50% { box-shadow: 0 2px 20px rgba(247, 105, 0, 0.28); }
}

.tutorial-fab.hidden {
    display: none;
}

/* --- Tutorial Card --- */
.tutorial {
    position: fixed;
    bottom: 64px;
    left: 50%;
    transform: translateX(-50%);
    width: 520px;
    max-width: calc(100vw - 32px);
    background: rgba(255, 255, 255, 0.96);
    backdrop-filter: blur(20px);
    -webkit-backdrop-filter: blur(20px);
    border: 1px solid rgba(0, 0, 0, 0.07);
    border-radius: 16px;
    box-shadow: 0 8px 40px rgba(0, 0, 0, 0.10), 0 0 0 1px rgba(0,0,0,0.02);
    z-index: 150;
    overflow: hidden;
    animation: tut-slide-up 0.3s cubic-bezier(0.22, 1, 0.36, 1);
}

@keyframes tut-slide-up {
    from { opacity: 0; transform: translateX(-50%) translateY(20px); }
    to { opacity: 1; transform: translateX(-50%) translateY(0); }
}

.tutorial.hidden {
    display: none;
}

.tutorial-header {
    display: flex;
    align-items: center;
    justify-content: space-between;
    padding: 10px 16px 0;
}

.tutorial-step-indicator {
    font-size: 0.7em;
    font-weight: 600;
    color: #9ca3af;
    letter-spacing: 0.03em;
}

.tutorial-close {
    width: 24px;
    height: 24px;
    border-radius: 6px;
    border: none;
    background: transparent;
    color: #9ca3af;
    font-size: 1.1em;
    cursor: pointer;
    display: flex;
    align-items: center;
    justify-content: center;
    transition: all 0.15s;
}

.tutorial-close:hover {
    background: rgba(0, 0, 0, 0.05);
    color: #374151;
}

.tutorial-body {
    padding: 8px 20px 12px;
    font-size: 0.88em;
    line-height: 1.6;
    color: #374151;
    max-height: 280px;
    overflow-y: auto;
}

.tutorial-title {
    font-size: 1.1em;
    font-weight: 600;
    color: #1f2937;
    margin-bottom: 6px;
}

.tutorial-body p {
    margin: 6px 0;
}

.tutorial-body ul {
    margin: 6px 0;
    padding-left: 20px;
}

.tutorial-body li {
    margin: 3px 0;
}

.tutorial-body code {
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.9em;
    background: rgba(247, 105, 0, 0.05);
    color: var(--brand);
    padding: 1px 5px;
    border-radius: 4px;
}

.tutorial-body kbd {
    display: inline-flex;
    align-items: center;
    justify-content: center;
    min-width: 18px;
    height: 18px;
    padding: 0 4px;
    border: 1px solid #e5e7eb;
    border-radius: 3px;
    background: #f9fafb;
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.85em;
    font-weight: 600;
    color: #6b7280;
    line-height: 1;
    vertical-align: middle;
}

.tutorial-body a {
    color: var(--brand);
    text-decoration: none;
    font-weight: 500;
}

.tutorial-body a:hover {
    text-decoration: underline;
}

.tut-note {
    color: #6b7280;
    font-style: italic;
    font-size: 0.93em;
}

.tut-beta {
    color: var(--sem-beta);
    font-family: 'JetBrains Mono', monospace;
}

.tut-alpha {
    color: var(--sem-alpha);
    font-family: 'JetBrains Mono', monospace;
}

.tut-var-bound {
    color: var(--sem-bound);
}

.tutorial-footer {
    display: flex;
    align-items: center;
    justify-content: space-between;
    padding: 8px 16px 12px;
    border-top: 1px solid rgba(0, 0, 0, 0.04);
}

.tutorial-dots {
    display: flex;
    gap: 5px;
    align-items: center;
}

.tutorial-dot {
    width: 6px;
    height: 6px;
    border-radius: 50%;
    background: #e5e7eb;
    cursor: pointer;
    transition: all 0.15s;
}

.tutorial-dot.active {
    background: var(--brand);
    transform: scale(1.3);
}

.tutorial-dot:hover {
    background: var(--brand-soft);
}

/* Tutorial: animated Space key indicator */
.tut-space-indicator {
    display: flex;
    gap: 8px;
    align-items: center;
    justify-content: center;
    padding: 8px 0;
    min-height: 36px;
}

.tut-space-key {
    display: inline-flex;
    align-items: center;
    justify-content: center;
    min-width: 52px;
    height: 28px;
    padding: 0 10px;
    border: 1px solid #d1d5db;
    border-radius: 6px;
    background: #f9fafb;
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.78em;
    font-weight: 600;
    color: #6b7280;
    box-shadow: 0 2px 0 #d1d5db;
    transition: transform 0.15s, box-shadow 0.15s, background 0.15s;
    opacity: 0;
    animation: tut-key-appear 0.3s ease-out forwards;
}

@keyframes tut-key-appear {
    from { opacity: 0; transform: translateY(-4px); }
    to { opacity: 1; transform: translateY(0); }
}

.tut-space-key.pressing {
    transform: translateY(2px);
    box-shadow: 0 0 0 #d1d5db;
    background: var(--brand-wash);
    border-color: var(--brand-pale);
    color: var(--brand);
}

.tut-space-key.pressed {
    transform: translateY(0);
    box-shadow: 0 2px 0 #d1d5db;
    background: #f9fafb;
    color: #6b7280;
}

/* Tutorial: Church-Rosser demo */
.tut-cr-demo {
    margin: 10px 0 6px;
    padding: 10px 12px;
    background: rgba(0, 0, 0, 0.02);
    border-radius: 8px;
    border: 1px solid rgba(0, 0, 0, 0.04);
    font-size: 0.9em;
}

.tut-cr-path {
    display: flex;
    align-items: flex-start;
    gap: 8px;
    margin-bottom: 8px;
}

.tut-cr-badge {
    display: inline-flex;
    align-items: center;
    padding: 2px 8px;
    border-radius: 4px;
    font-size: 0.72em;
    font-weight: 600;
    text-transform: uppercase;
    letter-spacing: 0.04em;
    background: var(--brand-wash);
    color: var(--brand);
    border: 1px solid var(--brand-pale);
    flex-shrink: 0;
    margin-top: 1px;
}

.tut-cr-steps {
    display: flex;
    flex-wrap: wrap;
    align-items: center;
    gap: 3px;
}

.tut-cr-term {
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.82em;
    color: #374151;
    padding: 1px 4px;
    border-radius: 3px;
    background: rgba(255, 255, 255, 0.6);
    opacity: 0;
    animation: tut-key-appear 0.3s ease-out forwards;
}

.tut-cr-term.nf {
    background: rgba(5, 150, 105, 0.08);
    color: #065f46;
    font-weight: 600;
    border: 1px solid rgba(5, 150, 105, 0.15);
}

.tut-cr-arrow {
    color: #9ca3af;
    font-size: 0.82em;
    opacity: 0;
    animation: tut-key-appear 0.2s ease-out forwards;
}

.tut-cr-result {
    margin-top: 8px;
    padding: 6px 10px;
    border-radius: 6px;
    font-size: 0.82em;
    color: #6b7280;
    background: rgba(0, 0, 0, 0.03);
    opacity: 0;
    animation: tut-key-appear 0.4s ease-out forwards;
}

.tut-cr-result.converges {
    background: rgba(5, 150, 105, 0.06);
    color: #065f46;
    border: 1px solid rgba(5, 150, 105, 0.12);
}

.tut-cr-result strong {
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.95em;
}

.tut-cr-waiting {
    color: #9ca3af;
    font-style: italic;
    font-size: 0.85em;
}

.tut-cr-status {
    margin: 8px 0;
}

.tut-cr-status code {
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.9em;
    background: rgba(247, 105, 0, 0.05);
    color: var(--brand);
    padding: 1px 5px;
    border-radius: 4px;
}

.tut-cr-prompt {
    padding: 10px 12px;
    background: rgba(0, 0, 0, 0.02);
    border-radius: 8px;
    border: 1px solid rgba(0, 0, 0, 0.04);
}

.tut-cr-prompt p {
    margin: 4px 0;
}

.tut-cr-prompt .btn {
    margin-top: 8px;
}

/* Main view: self-loop */
.main-self-loop-label {
    font-family: 'JetBrains Mono', monospace;
    font-size: 12px;
    font-weight: 600;
}

.tut-exit-actions {
    display: flex;
    gap: 8px;
    margin-top: 12px;
    justify-content: center;
}

.tut-exit-actions .btn {
    min-width: 120px;
}

.tutorial-start-btn {
    background: linear-gradient(135deg, var(--brand-tint) 0%, var(--brand-wash) 100%);
    border-color: var(--brand-pale);
    color: var(--brand-dark);
    font-weight: 600;
}

.tutorial-start-btn:hover {
    background: linear-gradient(135deg, var(--brand-wash) 0%, var(--brand-pale) 100%);
    border-color: var(--brand-soft);
}

/* --- Welcome Nudge --- */
.welcome-nudge {
    position: fixed;
    top: 16px;
    right: 64px;
    max-width: 380px;
    padding: 16px 20px;
    background: rgba(255, 255, 255, 0.96);
    backdrop-filter: blur(20px);
    -webkit-backdrop-filter: blur(20px);
    border: 1px solid rgba(247, 105, 0, 0.12);
    border-radius: 14px;
    box-shadow: 0 8px 32px rgba(247, 105, 0, 0.08), 0 0 0 1px rgba(0,0,0,0.02);
    z-index: 160;
    opacity: 0;
    transform: translateY(-8px);
    transition: opacity 0.3s, transform 0.3s cubic-bezier(0.22, 1, 0.36, 1);
}

.welcome-nudge.visible {
    opacity: 1;
    transform: translateY(0);
    transition: opacity 0.4s cubic-bezier(0.4, 0, 0.2, 1),
                transform 0.4s cubic-bezier(0.22, 1, 0.36, 1);
}

.welcome-text {
    font-size: 0.9em;
    line-height: 1.5;
    color: #374151;
    margin-bottom: 12px;
}

.welcome-text strong {
    color: var(--brand);
}

.welcome-actions {
    display: flex;
    align-items: center;
    gap: 6px;
}

/* --- Hint Bar --- */
#hint-bar {
    position: fixed;
    top: 14px;
    left: 60px;
    display: flex;
    gap: 14px;
    align-items: center;
    padding: 5px 12px;
    background: rgba(255, 255, 255, 0.82);
    backdrop-filter: blur(12px);
    -webkit-backdrop-filter: blur(12px);
    border: 1px solid rgba(0, 0, 0, 0.05);
    border-radius: 8px;
    z-index: 85;
    pointer-events: none;
}

.hint {
    display: flex;
    align-items: center;
    gap: 4px;
    font-size: 0.7em;
    color: #9ca3af;
    white-space: nowrap;
}

.hint kbd {
    display: inline-flex;
    align-items: center;
    justify-content: center;
    min-width: 18px;
    height: 17px;
    padding: 0 4px;
    border: 1px solid #e5e7eb;
    border-radius: 3px;
    background: #f9fafb;
    font-family: 'JetBrains Mono', monospace;
    font-size: 0.88em;
    font-weight: 600;
    color: #6b7280;
    line-height: 1;
}

/* --- Status Bar --- */
#status-bar {
    display: none;
}

/* --- Branding Watermark --- */
#branding {
    position: fixed;
    bottom: 16px;
    right: 18px;
    display: flex;
    align-items: center;
    gap: 5px;
    font-family: 'Inter', sans-serif;
    font-size: 0.68em;
    font-weight: 400;
    color: rgba(0, 0, 0, 0.18);
    letter-spacing: 0.02em;
    pointer-events: none;
    user-select: none;
    z-index: 1;
    transition: color 0.3s;
}

#branding .branding-course {
    font-family: 'JetBrains Mono', monospace;
    font-weight: 500;
    color: rgba(247, 105, 0, 0.22);
}

#branding .branding-sep {
    color: rgba(0, 0, 0, 0.12);
}

#branding:hover {
    color: rgba(0, 0, 0, 0.35);
}

#branding:hover .branding-course {
    color: rgba(247, 105, 0, 0.45);
}

/* --- Scrollbar --- */
::-webkit-scrollbar { width: 6px; }
::-webkit-scrollbar-track { background: transparent; }
::-webkit-scrollbar-thumb {
    background: #d1d5db;
    border-radius: 3px;
}

/* --- Responsive --- */

/* Tablet */
@media (max-width: 700px) {
    #input-bar {
        max-width: calc(100vw - 24px);
    }
    #input-bar .select { display: none; }
    .drawer { width: 260px; }
    #tree-panel { max-width: 220px; }
    .back-bar .back-text { display: none; }
    .back-bar { padding: 5px 8px; }

    .main-node-card { font-size: 16px; line-height: 1.6; }

    .tutorial { width: 440px; }
    .tutorial-body { font-size: 0.84em; max-height: 240px; }
}

/* Mobile */
@media (max-width: 540px) {
    /* Input bar: compact, avoid overlap with tutorial */
    #input-bar {
        max-width: calc(100vw - 16px);
        gap: 6px;
        padding: 5px 8px 5px 10px;
        border-radius: 10px;
    }
    #input-bar .logo { font-size: 18px; }
    .input-group { min-width: 0; }
    .input-group input { height: 30px; font-size: 0.78em; }
    .input-group .btn { height: 30px; padding: 0 10px; font-size: 0.78em; }
    #input-bar .select { display: none; }

    /* Term display: smaller for mobile screens */
    .main-node-card {
        font-size: 14px;
        line-height: 1.5;
        padding: 3px 6px;
    }

    /* Context menu: bigger touch targets */
    .ctx-btn {
        width: 48px;
        height: 48px;
        font-size: 1.3em;
    }
    #context-menu {
        gap: 8px;
        padding: 8px 10px;
    }

    /* Alpha popup: accommodate mobile keyboard */
    .alpha-popup {
        left: 50% !important;
        transform: translateX(-50%);
        top: auto !important;
        bottom: 64px;
    }
    .alpha-input { width: 80px; height: 34px; font-size: 1em; }

    /* Tutorial: fill width, above input bar */
    .tutorial {
        width: calc(100vw - 16px);
        bottom: 56px;
        border-radius: 12px;
    }
    .tutorial-body {
        padding: 6px 14px 10px;
        font-size: 0.82em;
        max-height: 200px;
        line-height: 1.5;
    }
    .tutorial-title { font-size: 1em; }
    .tutorial-header { padding: 8px 12px 0; }
    .tutorial-footer { padding: 6px 12px 8px; }
    .tutorial-footer .btn { height: 30px; padding: 0 10px; font-size: 0.75em; }
    .tutorial-dot { width: 8px; height: 8px; }
    .tutorial-dot.active { transform: scale(1.2); }

    /* Tutorial FAB: avoid overlap with back bar */
    .tutorial-fab { top: 14px; right: 52px; }

    /* Hint bar: hide on mobile (keyboard shortcuts not applicable) */
    #hint-bar { display: none; }

    /* Drawer: full width on mobile */
    .drawer { width: 100vw; }

    /* Tree panel: smaller on mobile */
    #tree-panel {
        max-width: 200px;
        max-height: 200px;
        bottom: 56px;
        left: 8px;
    }
    .dtree-text { max-width: 140px; font-size: 0.62em; }

    /* Welcome nudge: below back bar, not overlapping tutorial fab */
    .welcome-nudge {
        top: auto;
        bottom: 56px;
        right: 8px;
        left: 8px;
        max-width: none;
    }

    /* Tree callout: repositioned for mobile */
    .tree-callout {
        bottom: 170px;
        left: 8px;
    }
    .tree-callout-text { font-size: 0.72em; }

    /* Branding: hide on small screens */
    #branding { display: none; }

    /* Back bar: just arrow */
    .back-bar .back-text { display: none; }
    .back-bar { padding: 5px 8px; }
}

/* Very small phones */
@media (max-width: 380px) {
    .main-node-card { font-size: 12px; }
    .tutorial-body { max-height: 160px; }
    #tree-panel { display: none; }
}

/* Touch-friendly: disable hover effects on touch devices */
@media (hover: none) {
    .term.has-op { cursor: default; }
    .term.has-op.hovered {
        background: rgba(247, 105, 0, 0.08);
        box-shadow: 0 0 0 2.5px rgba(247, 105, 0, 0.18);
    }
    .ctx-btn:hover { transform: none; }
    .ctx-btn:active { transform: scale(0.94); }
    #viewport { cursor: default; touch-action: none; }
    #viewport.dragging { cursor: default; }
}

/* Prevent double-tap zoom on interactive elements */
.ctx-btn, .btn, .tutorial-dot, .dtree-label, .strategy-btn, .mobile-step-fab {
    touch-action: manipulation;
}

/* --- Mobile Step FAB --- */
.mobile-step-fab {
    position: fixed;
    bottom: 56px;
    right: 14px;
    width: 52px;
    height: 52px;
    border-radius: 50%;
    border: 2px solid var(--brand-soft);
    background: linear-gradient(135deg, #fff 0%, var(--brand-wash) 100%);
    cursor: pointer;
    display: flex;
    align-items: center;
    justify-content: center;
    z-index: 100;
    box-shadow: 0 4px 20px rgba(247, 105, 0, 0.18);
    transition: all 0.15s cubic-bezier(0.4, 0, 0.2, 1);
}

.mobile-step-fab:active {
    transform: scale(0.9);
    background: var(--brand-wash);
}

.mobile-step-fab:disabled {
    opacity: 0.35;
    pointer-events: none;
}

.mobile-step-fab.hidden { display: none; }

.mobile-step-icon {
    font-size: 20px;
    color: var(--brand);
    line-height: 1;
    margin-left: 2px;
}

/* Show mobile FAB only on touch devices */
@media (hover: none) {
    .mobile-step-fab:not(.hidden) { display: flex; }
}

/* When tutorial is open on mobile, shift step FAB up */
@media (max-width: 540px) {
    .mobile-step-fab { bottom: 52px; right: 10px; width: 46px; height: 46px; }
    .mobile-step-icon { font-size: 17px; }

    /* Safe area support for iPhone notch/home indicator */
    #input-bar {
        bottom: calc(8px + env(safe-area-inset-bottom, 0px));
    }
    .tutorial {
        bottom: calc(52px + env(safe-area-inset-bottom, 0px));
    }
    .mobile-step-fab {
        bottom: calc(48px + env(safe-area-inset-bottom, 0px));
    }
    #tree-panel {
        bottom: calc(52px + env(safe-area-inset-bottom, 0px));
    }
}