fix

Author: felixpernegger

packages/viewer/src/components/Dev/Explore.svelte

@@ -1,20 +1,10 @@
 <script lang="ts">
   import context from '@/context'
   import Log from './Log.svelte'
-  import { defaultStorage } from '@/repositories'
   import { reset } from '@/util'
+  import { showLeanLinks, showRedundancy } from '@/stores/settings'
 
   const { spaces, properties, theorems, traits } = context()
-
-  let showRedundancy = defaultStorage.getItem('showRedundancy') !== null
-  $: showRedundancy
-    ? defaultStorage.setItem('showRedundancy', 'show')
-    : defaultStorage.removeItem('showRedundancy')
-
-  let showLeanLinks = defaultStorage.getItem('showLeanLinks') !== null
-  $: showLeanLinks
-    ? defaultStorage.setItem('showLeanLinks', 'show')
-    : defaultStorage.removeItem('showLeanLinks')
 </script>
 
 <h4>Entities</h4>
@@ -52,7 +42,7 @@
         <input
           id="redundancyCheckbox"
           type="checkbox"
-          bind:checked={showRedundancy}
+          bind:checked={$showRedundancy}
         />
         <label for="redundancyCheckbox"> Show redundancies in tables </label>
       </td>
@@ -62,7 +52,7 @@
         <input
           id="leanLinksCheckbox"
           type="checkbox"
-          bind:checked={showLeanLinks}
+          bind:checked={$showLeanLinks}
         />
         <label for="leanLinksCheckbox">
           Show Lean formalisation links (experimental)

packages/viewer/src/components/Shared/LeanLink.svelte

@@ -1,9 +1,15 @@
 <script context="module" lang="ts">
   const repo = 'felixpernegger/pibase-lean'
 
-  const directories: Record<string, Promise<Set<string>>> = {
-    property: fetchDirectory('PiBaseLean/Properties'),
-    theorem: fetchDirectory('PiBaseLean/Theorems'),
+  const cache: Record<string, Promise<Set<string>>> = {}
+
+  function getDirectory(kind: 'property' | 'theorem'): Promise<Set<string>> {
+    const path =
+      kind === 'property' ? 'PiBaseLean/Properties' : 'PiBaseLean/Theorems'
+    if (!cache[kind]) {
+      cache[kind] = fetchDirectory(path)
+    }
+    return cache[kind]
   }
 
   async function fetchDirectory(path: string): Promise<Set<string>> {
@@ -21,14 +27,12 @@
 </script>
 
 <script lang="ts">
-  import { onMount } from 'svelte'
   import { Icons } from '@/components/Shared'
-  import { defaultStorage } from '@/repositories'
+  import { showLeanLinks } from '@/stores/settings'
 
   export let kind: 'property' | 'theorem'
   export let id: number
 
-  let enabled = defaultStorage.getItem('showLeanLinks') !== null
   let loaded = false
   let available = false
 
@@ -38,18 +42,15 @@
     kind === 'property' ? 'PiBaseLean/Properties' : 'PiBaseLean/Theorems'
   $: href = `https://github.com/${repo}/blob/master/${basePath}/${folderName}/${file}`
 
-  onMount(async () => {
-    if (!enabled) {
+  $: if ($showLeanLinks && !loaded) {
+    getDirectory(kind).then(ids => {
+      available = ids.has(folderName)
       loaded = true
-      return
-    }
-    const ids = await directories[kind]
-    available = ids.has(folderName)
-    loaded = true
-  })
+    })
+  }
 </script>
 
-{#if enabled && loaded}
+{#if $showLeanLinks && loaded}
   {#if available}
     <div>
       <a {href} target="_blank" rel="noopener noreferrer">

packages/viewer/src/components/Traits/Related.svelte

@@ -5,8 +5,8 @@
   import context from '@/context'
   import type { Property, Space, Trait, Traits } from '@/models'
   import FilterButtons from './FilterButtons.svelte'
-  import { defaultStorage } from '@/repositories'
   import { writable } from 'svelte/store'
+  import { showRedundancy } from '@/stores/settings'
   import urlSearchParam from '@/stores/urlSearchParam'
   import { checkIfRedundant } from '@/stores/deduction'
 
@@ -21,8 +21,6 @@
   let filterMode: 'all' | 'known' | 'asserted' | 'true' | 'false' | 'missing'
   filterMode = 'known'
 
-  let showRedundancy = defaultStorage.getItem('showRedundancy') != null
-
   $: all = related($traits)
   // all has type [Space, Property, Trait][]
   // we need to index names in different positions depending on which kind we
@@ -109,10 +107,9 @@
           <Link.Trait {space} {property}>
             <SourceIcon
               value={trait?.asserted}
-              redundant={showRedundancy &&
+              redundant={$showRedundancy &&
                 trait?.asserted &&
                 checkIfRedundant(space, property, $theorems, $traits).redundant}
-              icon="user"
             />
           </Link.Trait>
         </td>

packages/viewer/src/stores/settings.test.ts

@@ -0,0 +1,85 @@
+import { beforeEach, describe, expect, it } from 'vitest'
+import { get } from 'svelte/store'
+import { persistedBoolean, showLeanLinks, showRedundancy } from './settings'
+
+function mockStorage() {
+  const data: Record<string, string> = {}
+  return {
+    data,
+    getItem: (key: string) => data[key] ?? null,
+    setItem: (key: string, value: string) => {
+      data[key] = value
+    },
+    removeItem: (key: string) => {
+      delete data[key]
+    },
+  }
+}
+
+describe('persistedBoolean', () => {
+  it('defaults to the given default value when storage is empty', () => {
+    const storage = mockStorage()
+    const store = persistedBoolean('flag', false, storage)
+    expect(get(store)).toBe(false)
+  })
+
+  it('initializes to true when the key already exists in storage', () => {
+    const storage = mockStorage()
+    storage.data['flag'] = 'show'
+    const store = persistedBoolean('flag', false, storage)
+    expect(get(store)).toBe(true)
+  })
+
+  it('writes to storage when set to true', () => {
+    const storage = mockStorage()
+    const store = persistedBoolean('flag', false, storage)
+    store.set(true)
+    expect(storage.data['flag']).toBe('show')
+  })
+
+  it('removes from storage when set to false', () => {
+    const storage = mockStorage()
+    storage.data['flag'] = 'show'
+    const store = persistedBoolean('flag', true, storage)
+    store.set(false)
+    expect(storage.data['flag']).toBeUndefined()
+  })
+
+  it('reflects updates via subscribe', () => {
+    const storage = mockStorage()
+    const store = persistedBoolean('flag', false, storage)
+    const values: boolean[] = []
+    store.subscribe(v => values.push(v))
+
+    store.set(true)
+    store.set(false)
+
+    expect(values).toEqual([false, true, false])
+  })
+})
+
+describe('showLeanLinks', () => {
+  it('defaults to false', () => {
+    expect(get(showLeanLinks)).toBe(false)
+  })
+
+  it('can be toggled', () => {
+    showLeanLinks.set(true)
+    expect(get(showLeanLinks)).toBe(true)
+    showLeanLinks.set(false)
+    expect(get(showLeanLinks)).toBe(false)
+  })
+})
+
+describe('showRedundancy', () => {
+  it('defaults to false', () => {
+    expect(get(showRedundancy)).toBe(false)
+  })
+
+  it('can be toggled', () => {
+    showRedundancy.set(true)
+    expect(get(showRedundancy)).toBe(true)
+    showRedundancy.set(false)
+    expect(get(showRedundancy)).toBe(false)
+  })
+})

packages/viewer/src/stores/settings.ts

@@ -0,0 +1,25 @@
+import { writable } from 'svelte/store'
+import { defaultStorage } from '@/repositories'
+
+export function persistedBoolean(
+  key: string,
+  defaultValue: boolean,
+  storage: Pick<Storage, 'getItem' | 'setItem' | 'removeItem'> = defaultStorage,
+) {
+  const store = writable<boolean>(
+    storage.getItem(key) !== null ? true : defaultValue,
+  )
+
+  store.subscribe(v => {
+    if (v) {
+      storage.setItem(key, 'show')
+    } else {
+      storage.removeItem(key)
+    }
+  })
+
+  return store
+}
+
+export const showLeanLinks = persistedBoolean('showLeanLinks', false)
+export const showRedundancy = persistedBoolean('showRedundancy', false)