ftml_viewer_components/components/
proofs.rs

1use 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        /*
121        #[cfg(any(feature = "csr", feature = "hydrate"))]
122        let s = {
123            let e = &*orig;
124            //leptos::web_sys::console::log_1(e);
125            let s = e.inner_html();
126            //tracing::info!("HTML: {s}");
127            s
128        };
129        #[cfg(not(any(feature = "csr", feature = "hydrate")))]
130        let s = String::new(); */
131        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        /*
146        #[cfg(any(feature = "csr", feature = "hydrate"))]
147        let s = {
148            let e = &*orig;
149            //leptos::web_sys::console::log_1(e);
150            let s = e.inner_html();
151            //tracing::info!("HTML: {s}");
152            s
153        };
154        #[cfg(not(any(feature = "csr", feature = "hydrate")))]
155        let s = String::new();
156         */
157        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        /*tracing::info!("Here 1:");
169        #[cfg(any(feature = "csr", feature = "hydrate"))]
170        let s = {
171            let e = &*orig;
172            //leptos::web_sys::console::log_1(e);
173            let s = e.inner_html();
174            //tracing::info!("HTML: {s}");
175            s
176        };
177        #[cfg(not(any(feature = "csr", feature = "hydrate")))]
178        let s = String::new();
179        */
180        body.set(orig);
181        Either::Left(())
182    } else {
183        Either::Right(view!(<DomCont orig cont=crate::iterate skip_head=true/>))
184    }
185}