UI changes

Author: StevenClontz

packages/viewer/src/components/Properties/Show.svelte

@@ -19,7 +19,10 @@
   const tabs = ['theorems', 'spaces', 'references'] as const
 </script>
 
-<h3>Property <Link.Property {property} content="idLong" /></h3>
+<h3>
+  Property <Link.Property {property} content="idLong" />
+  <LeanLink kind="property" id={property.id} />
+</h3>
 
 <h1>
   <Typeset body={property.name} />
@@ -39,8 +42,6 @@
   <Source source={property.description} internal external />
 </section>
 
-<LeanLink kind="property" id={property.id} />
-
 <Tabs {tabs} {tab} {rel} />
 
 {#if tab === 'spaces'}

packages/viewer/src/components/Shared/Icons/Lean.svelte

@@ -0,0 +1,14 @@
+<svg
+  width="70"
+  height="20"
+  viewBox="0 0 486 169"
+  xmlns="http://www.w3.org/2000/svg"
+  stroke="auto"
+  fill="transparent"
+  stroke-width="10"
+  ><path
+    d="M206.333 5.67949H105.667M206.333 5.67949L243.25 84.5M206.333 5.67949V84.5M243.25 84.5H317.549M243.25 84.5L279.667 163.321L280.889 163.318L317.549 84.5M206.333 84.5V163.321H5V5M206.333 84.5H105.667M317.549 84.5L353 5.67949M353 5.67949V164M353 5.67949H353.667L480.333 163.454H481V5"
+    stroke-linecap="round"
+    stroke-linejoin="round"
+  /></svg
+>

packages/viewer/src/components/Shared/Icons/index.ts

@@ -1,6 +1,7 @@
 export { default as Branch } from './Branch.svelte'
 export { default as Check } from './Check.svelte'
 export { default as Dice } from './Dice.svelte'
+export { default as Lean } from './Lean.svelte'
 export { default as Question } from './Question.svelte'
 export { default as Repeat } from './Repeat.svelte'
 export { default as Search } from './Search.svelte'

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

@@ -22,6 +22,7 @@
 
 <script lang="ts">
   import { onMount } from 'svelte'
+  import { Icons } from '@/components/Shared'
 
   export let kind: 'property' | 'theorem'
   export let id: number
@@ -43,13 +44,30 @@
 </script>
 
 {#if loaded}
-  <p>
-    {#if available}
+  {#if available}
+    <div>
       <a {href} target="_blank" rel="noopener noreferrer">
-        Formalisation available.
+        <Icons.Lean />
       </a>
-    {:else}
-      No formalisation available.
-    {/if}
-  </p>
+    </div>
+  {/if}
 {/if}
+
+<style>
+  div {
+    display: inline-block;
+    border: 1px solid white;
+    padding: 2px;
+  }
+  div:hover {
+    background: #f6fafe;
+    border: 1px solid #e0edfb;
+    border-radius: 5px;
+  }
+  a {
+    padding: 5px;
+    display: flex;
+    align-items: center;
+    justify-content: center;
+  }
+</style>

packages/viewer/src/components/Theorems/Show.svelte

@@ -11,7 +11,10 @@
   const tabs = ['converse', 'references'] as const
 </script>
 
-<h3>Theorem <Link.Theorem {theorem} content="idLong" /></h3>
+<h3>
+  Theorem <Link.Theorem {theorem} content="idLong" />
+  <LeanLink kind="theorem" id={theorem.id} />
+</h3>
 
 <h1>
   <Name {theorem} />
@@ -25,8 +28,6 @@
   <Source source={theorem.description} internal external />
 </section>
 
-<LeanLink kind="theorem" id={theorem.id} />
-
 <Tabs {tabs} {tab} {rel} />
 
 {#if tab === 'converse'}