ftml_viewer_components/components/
proofs.rs1use flams_ontology::{narration::paragraphs::ParagraphKind, uris::DocumentElementURI};
2use leptos::{context::Provider, either::Either, prelude::*};
3use leptos_posthoc::{DomCont, OriginalNode};
4
5use crate::ts::FragmentContinuation;
6
7#[derive(Copy, Clone, Default)]
8struct Elem(RwSignal<Option<std::sync::Mutex<Option<OriginalNode>>>>);
9impl Elem {
10 fn set(&self, node: OriginalNode) {
11 self.0.set(Some(std::sync::Mutex::new(Some(node))))
12 }
13 fn get(&self) -> Option<OriginalNode> {
14 self.0.with(|v| {
15 v.as_ref()
16 .and_then(|l| l.lock().ok().and_then(|mut v| (&mut *v).take()))
17 })
18 }
19}
20
21#[derive(Copy, Clone)]
22struct ProofOrSubproof {
23 sub: bool,
24 expanded: RwSignal<bool>,
25 title: Elem,
26 body: Elem,
27}
28
29pub fn proof<V: IntoView + 'static>(
30 uri: DocumentElementURI,
31 initial: bool,
32 children: impl FnOnce() -> V + Send + 'static,
33) -> impl IntoView {
34 let value = ProofOrSubproof {
35 sub: false,
36 expanded: RwSignal::new(!initial),
37 title: Elem::default(),
38 body: Elem::default(),
39 };
40 let display = Memo::new(move |_| {
41 if value.expanded.get() {
42 "display:contents;"
43 } else {
44 "display:none;"
45 }
46 });
47 let cls = Memo::new(move |_| {
48 if value.expanded.get() {
49 "ftml-proof-title ftml-proof-title-expanded"
50 } else {
51 "ftml-proof-title ftml-proof-title-collapsed"
52 }
53 });
54 FragmentContinuation::wrap(
55 &(uri, ParagraphKind::Proof.into()),
56 view! {
57 <Provider value=Some(value)>
58 {children()}
59 </Provider>
60 {move || value.title.get().map(|html| {
61 view!(<div class=cls on:click=move |_| value.expanded.update(|b| *b = !*b)>
62 <DomCont orig=html cont=crate::iterate skip_head=true />
63 </div>)
64 })}
65 {move || value.body.get().map(|html|
66 view!{<div style=display><DomCont orig=html cont=crate::iterate skip_head=true /></div>}
67 )}
68 },
69 )
70}
71
72pub fn subproof<V: IntoView + 'static>(
73 uri: DocumentElementURI,
74 initial: bool,
75 children: impl FnOnce() -> V + Send + 'static,
76) -> impl IntoView {
77 let value = ProofOrSubproof {
78 sub: true,
79 expanded: RwSignal::new(!initial),
80 title: Elem::default(),
81 body: Elem::default(),
82 };
83 let display = Memo::new(move |_| {
84 if value.expanded.get() {
85 "display:contents;"
86 } else {
87 "display:none;"
88 }
89 });
90 let cls = Memo::new(move |_| {
91 if value.expanded.get() {
92 "ftml-subproof-title ftml-proof-title-expanded"
93 } else {
94 "ftml-subproof-title ftml-proof-title-collapsed"
95 }
96 });
97 FragmentContinuation::wrap(
98 &(uri, ParagraphKind::Proof.into()),
99 view! {
100 <Provider value=Some(value)>
101 {children()}
102 </Provider>
103 {move || value.title.get().map(|html| {
104 view!(<div class=cls on:click=move |_| value.expanded.update(|b| *b = !*b)>
105 <DomCont orig=html cont=crate::iterate skip_head=true />
106 </div>)
107 })}
108 {move || value.body.get().map(|html|
109 view!{<div style=display><DomCont orig=html cont=crate::iterate skip_head=true /></div>}
110 )}
111 },
112 )
113}
114
115pub fn proof_title(orig: OriginalNode) -> impl IntoView {
116 if let Some(Some(ProofOrSubproof {
117 title, sub: false, ..
118 })) = use_context::<Option<ProofOrSubproof>>()
119 {
120 title.set(orig);
132 Either::Left(())
133 } else {
134 Either::Right(view! {
135 <div class="ftml-proof-title"><DomCont orig cont=crate::iterate skip_head=true/></div>
136 })
137 }
138}
139
140pub fn subproof_title(orig: OriginalNode) -> impl IntoView {
141 if let Some(Some(ProofOrSubproof {
142 title, sub: true, ..
143 })) = use_context::<Option<ProofOrSubproof>>()
144 {
145 title.set(orig);
158 Either::Left(())
159 } else {
160 Either::Right(view! {
161 <div class="ftml-subproof-title"><DomCont orig cont=crate::iterate skip_head=true/></div>
162 })
163 }
164}
165
166pub fn proof_body(orig: OriginalNode) -> impl IntoView {
167 if let Some(Some(ProofOrSubproof { body, .. })) = use_context::<Option<ProofOrSubproof>>() {
168 body.set(orig);
181 Either::Left(())
182 } else {
183 Either::Right(view!(<DomCont orig cont=crate::iterate skip_head=true/>))
184 }
185}