ftml_viewer_components/components/omdoc/
content.rs

1use crate::{
2    components::{IntoLOs, LOs},
3    FTMLString, FTMLStringMath,
4};
5use flams_ontology::{
6    content::{declarations::symbols::ArgSpec, terms::Term},
7    languages::Language,
8    uris::{ContentURITrait, ModuleURI, Name, SymbolURI, URIOrRefTrait, URIRefTrait, URI},
9};
10use flams_utils::vecmap::VecSet;
11
12use super::{narration::OMDocDocumentElement, OMDoc, OMDocDecl};
13use flams_web_utils::{
14    components::{Block, Header, HeaderLeft, HeaderRight, LazyCollapsible},
15    inject_css,
16};
17use leptos::{
18    context::Provider,
19    either::{Either, EitherOf5},
20    prelude::*,
21};
22use thaw::{Text, TextTag};
23
24#[derive(Copy, Clone)]
25struct InStruct;
26
27#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
28#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
29pub struct OMDocModule<E: OMDocDecl> {
30    pub uri: ModuleURI,
31    #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
32    pub imports: VecSet<ModuleURI>,
33    #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
34    pub uses: VecSet<ModuleURI>,
35    pub metatheory: Option<ModuleURI>,
36    pub signature: Option<Language>,
37    pub children: Vec<E>,
38}
39impl<E: OMDocDecl> super::OMDocT for OMDocModule<E> {
40    fn into_view(self) -> impl IntoView {
41        view! {
42            <Block>
43                <Header slot><b>"Module "
44                    {super::module_name(&self.uri)}
45                    {self.metatheory.map(|m|
46                        view!(" (Metatheory "{super::module_name(&m)}")")
47                    )}
48                </b></Header>
49                <HeaderLeft slot>{super::uses("Imports",self.imports.0)}</HeaderLeft>
50                <HeaderRight slot>{super::uses("Uses",self.uses.0)}</HeaderRight>
51                {self.children.into_iter().map(super::OMDocT::into_view).collect_view()}
52            </Block>
53        }
54    }
55}
56impl From<OMDocModule<OMDocDeclaration>> for OMDoc {
57    #[inline]
58    fn from(value: OMDocModule<OMDocDeclaration>) -> Self {
59        Self::Module(value)
60    }
61}
62impl From<OMDocModule<OMDocDocumentElement>> for OMDoc {
63    #[inline]
64    fn from(value: OMDocModule<OMDocDocumentElement>) -> Self {
65        Self::DocModule(value)
66    }
67}
68impl From<OMDocModule<OMDocDeclaration>> for OMDocDeclaration {
69    #[inline]
70    fn from(value: OMDocModule<OMDocDeclaration>) -> Self {
71        Self::NestedModule(value)
72    }
73}
74
75#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
76#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
77pub struct OMDocMorphism<E: OMDocDecl> {
78    pub uri: SymbolURI,
79    pub total: bool,
80    pub target: Option<ModuleURI>,
81    #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
82    pub uses: VecSet<ModuleURI>,
83    pub children: Vec<E>,
84}
85impl<E: OMDocDecl> super::OMDocT for OMDocMorphism<E> {
86    fn into_view(self) -> impl IntoView {
87        view!(<div>"TODO: Morphism"</div>)
88    }
89}
90impl From<OMDocMorphism<OMDocDeclaration>> for OMDoc {
91    #[inline]
92    fn from(value: OMDocMorphism<OMDocDeclaration>) -> Self {
93        Self::Morphism(value)
94    }
95}
96impl From<OMDocMorphism<OMDocDocumentElement>> for OMDoc {
97    #[inline]
98    fn from(value: OMDocMorphism<OMDocDocumentElement>) -> Self {
99        Self::DocMorphism(value)
100    }
101}
102impl From<OMDocMorphism<OMDocDeclaration>> for OMDocDeclaration {
103    #[inline]
104    fn from(value: OMDocMorphism<OMDocDeclaration>) -> Self {
105        Self::Morphism(value)
106    }
107}
108
109#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
110#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
111pub struct OMDocStructure<E: OMDocDecl> {
112    pub uri: SymbolURI,
113    pub macro_name: Option<String>,
114    #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
115    pub uses: VecSet<ModuleURI>,
116    #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
117    pub extends: VecSet<ModuleURI>,
118    pub children: Vec<E>,
119    pub extensions: Vec<(SymbolURI, Vec<OMDocSymbol>)>,
120}
121impl<E: OMDocDecl> super::OMDocT for OMDocStructure<E> {
122    fn into_view(self) -> impl IntoView {
123        let OMDocStructure {
124            uri,
125            macro_name,
126            extends,
127            extensions,
128            uses,
129            children,
130        } = self;
131        let uriclone = uri.clone();
132        view! {
133            <Provider value=InStruct>
134                <Block>
135                    <Header slot><span>
136                        <b>"Structure "{super::symbol_name(&uri, uri.name().last_name().as_ref())}</b>
137                        {macro_name.map(|name| view!(<span>" ("<Text tag=TextTag::Code>"\\"{name}</Text>")"</span>))}
138                    </span></Header>
139                    <HeaderLeft slot>{super::uses("Extends",extends.0)}</HeaderLeft>
140                    <HeaderRight slot>{super::uses("Uses",uses.0)}</HeaderRight>
141                    {children.into_iter().map(super::OMDocT::into_view).collect_view()}
142                    {if !extensions.is_empty() {Some(view!{
143                        <b>"Conservative Extensions:"</b>
144                        {extensions.into_iter().map(|(uri,s)| view!{
145                            <Block show_separator=false>
146                                <Header slot>{super::module_name(uri.module())}</Header>
147                                {s.into_iter().map(super::OMDocT::into_view).collect_view()}
148                            </Block>
149                        }).collect_view()}
150                    })} else {None}}
151                    {do_los(uriclone)}
152                </Block>
153            </Provider>
154        }
155    }
156}
157impl From<OMDocStructure<OMDocDeclaration>> for OMDoc {
158    #[inline]
159    fn from(value: OMDocStructure<OMDocDeclaration>) -> Self {
160        Self::Structure(value)
161    }
162}
163impl From<OMDocStructure<OMDocDocumentElement>> for OMDoc {
164    #[inline]
165    fn from(value: OMDocStructure<OMDocDocumentElement>) -> Self {
166        Self::DocStructure(value)
167    }
168}
169impl From<OMDocStructure<OMDocDeclaration>> for OMDocDeclaration {
170    #[inline]
171    fn from(value: OMDocStructure<OMDocDeclaration>) -> Self {
172        Self::Structure(value)
173    }
174}
175
176#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
177#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
178pub struct OMDocExtension<E: OMDocDecl> {
179    pub uri: SymbolURI,
180    pub target: SymbolURI,
181    #[cfg_attr(feature = "ts", tsify(type = "ModuleURI[]"))]
182    pub uses: VecSet<ModuleURI>,
183    pub children: Vec<E>,
184}
185impl<E: OMDocDecl> super::OMDocT for OMDocExtension<E> {
186    fn into_view(self) -> impl IntoView {
187        let OMDocExtension {
188            uri,
189            target,
190            uses,
191            children,
192        } = self;
193        view! {
194            <Provider value=InStruct>
195                <Block>
196                    <Header slot><span>
197                        <b>"Conservative Extension for "{super::symbol_name(&target, target.name().last_name().as_ref())}</b>
198                    </span></Header>
199                    <HeaderRight slot>{super::uses("Uses",uses.0)}</HeaderRight>
200                    {children.into_iter().map(super::OMDocT::into_view).collect_view()}
201                </Block>
202            </Provider>
203        }
204    }
205}
206impl From<OMDocExtension<OMDocDeclaration>> for OMDoc {
207    #[inline]
208    fn from(value: OMDocExtension<OMDocDeclaration>) -> Self {
209        Self::Extension(value)
210    }
211}
212impl From<OMDocExtension<OMDocDocumentElement>> for OMDoc {
213    #[inline]
214    fn from(value: OMDocExtension<OMDocDocumentElement>) -> Self {
215        Self::DocExtension(value)
216    }
217}
218impl From<OMDocExtension<OMDocDeclaration>> for OMDocDeclaration {
219    #[inline]
220    fn from(value: OMDocExtension<OMDocDeclaration>) -> Self {
221        Self::Extension(value)
222    }
223}
224
225#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
226#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
227#[cfg_attr(feature = "ts", tsify(into_wasm_abi, from_wasm_abi))]
228#[serde(tag = "type")]
229pub enum OMDocDeclaration {
230    Symbol(OMDocSymbol),
231    NestedModule(OMDocModule<OMDocDeclaration>),
232    Structure(OMDocStructure<OMDocDeclaration>),
233    Morphism(OMDocMorphism<OMDocDeclaration>),
234    Extension(OMDocExtension<OMDocDeclaration>),
235}
236
237impl super::sealed::Sealed for OMDocDeclaration {}
238impl super::OMDocDecl for OMDocDeclaration {}
239impl super::OMDocT for OMDocDeclaration {
240    #[inline]
241    fn into_view(self) -> impl IntoView {
242        match self {
243            Self::Symbol(e) => EitherOf5::A(e.into_view()),
244            Self::NestedModule(e) => EitherOf5::B(e.into_view()),
245            Self::Structure(e) => EitherOf5::C(e.into_view()),
246            Self::Morphism(e) => EitherOf5::D(e.into_view()),
247            Self::Extension(e) => EitherOf5::E(e.into_view()),
248        }
249    }
250}
251impl From<OMDocDeclaration> for OMDoc {
252    #[inline]
253    fn from(value: OMDocDeclaration) -> Self {
254        match value {
255            OMDocDeclaration::Symbol(s) => Self::SymbolDeclaration(s),
256            OMDocDeclaration::NestedModule(s) => Self::Module(s),
257            OMDocDeclaration::Structure(s) => Self::Structure(s),
258            OMDocDeclaration::Morphism(s) => Self::Morphism(s),
259            OMDocDeclaration::Extension(s) => Self::Extension(s),
260        }
261    }
262}
263
264pub(super) fn do_notations(uri: URI, arity: ArgSpec) -> impl IntoView {
265    use flams_web_utils::components::{Popover, PopoverTrigger};
266    use thaw::{Table, TableCell, TableHeader, TableHeaderCell, TableRow};
267    let functional = arity.num() > 0;
268    let as_variable = match &uri {
269        URI::Content(_) => false,
270        URI::Narrative(_) => true,
271        _ => unreachable!(),
272    };
273    let uriclone = uri.clone();
274    inject_css("flams-notation-table", include_str!("notations.css"));
275    crate::remote::get!(notations(uri.clone()) = v => {
276        let uri = uriclone.clone();
277        if v.is_empty() {None} else {
278            Some(view!{
279                <div>
280                    <Table class="flams-notation-table"><TableRow>
281                    <TableCell class="flams-notation-header"><span>"Notations: "</span></TableCell>
282                    {let uri = uri;v.into_iter().map(move |(u,n)| {
283                        let html = n.display_ftml(false,as_variable,&uri).to_string();
284                        let htmlclone = html.clone();
285                        let uri = uri.clone();
286                        view!{
287                            <TableCell class="flams-notation-cell">
288                                <Popover>
289                                    <PopoverTrigger slot><span>
290                                        <Provider value=crate::components::terms::DisablePopover>
291                                            <FTMLStringMath html/>
292                                        </Provider>
293                                    </span></PopoverTrigger>
294                                    {
295                                        let html = htmlclone;
296                                        let op = if functional {
297                                            n.op.as_ref().map(|op| op.display_ftml(as_variable,&uri).to_string())
298                                        } else {None};
299                                        view!{<Table class="flams-notation-table">
300                                            <TableHeader>
301                                                <TableRow>
302                                                    <TableHeaderCell class="flams-notation-header">"source document"</TableHeaderCell>
303                                                    {if functional {Some(view!{<TableHeaderCell class="flams-notation-header">"operation"</TableHeaderCell>})} else {None}}
304                                                    <TableHeaderCell class="flams-notation-header">"notation"</TableHeaderCell>
305                                                </TableRow>
306                                            </TableHeader>
307                                            <TableRow>
308                                                <TableCell class="flams-notation-cell">{
309                                                    super::doc_name(u.document(), u.document().name().last_name().to_string())
310                                                }</TableCell>
311                                                {if functional {Some(view!{<TableCell class="flams-notation-cell">{
312                                                    op.map_or_else(
313                                                        || Either::Left("(No op)"),
314                                                        |html| Either::Right(view!{
315                                                            <Provider value=crate::components::terms::DisablePopover>
316                                                                <FTMLStringMath html/>
317                                                            </Provider>
318                                                        })
319                                                    )
320                                                }</TableCell>})} else {None}}
321                                                <TableCell class="flams-notation-cell">
322                                                    <Provider value=crate::components::terms::DisablePopover>
323                                                        <FTMLStringMath html/>
324                                                    </Provider>
325                                                </TableCell>
326                                            </TableRow>
327                                        </Table>}
328                                    }
329                                </Popover>
330                            </TableCell>
331                        }
332                    }).collect_view()}
333                    </TableRow></Table>
334                </div>
335            })
336        }
337    })
338}
339
340fn do_los(uri: SymbolURI) -> impl IntoView {
341    use flams_ontology::narration::LOKind;
342    view! {
343        <LazyCollapsible>
344            <Header slot><span>"Learning Objects"</span></Header>
345            <div style="padding-left:15px">{
346                let uri = uri.clone();
347                crate::remote::get!(get_los(uri.clone(),true) = v => {
348                    let LOs {definitions,examples,problems} = v.lo_sort();
349                    view!{
350                        <div>{if definitions.is_empty() { None } else {Some(
351                            super::comma_sep("Definitions", definitions.into_iter().map(|uri| {
352                                let title = uri.name().last_name().to_string();
353                                super::doc_elem_name(uri,None,title)
354                            }))
355                        )}}</div>
356                        <div>{if examples.is_empty() { None } else {Some(
357                            super::comma_sep("Examples", examples.into_iter().map(|uri| {
358                                let title = uri.name().last_name().to_string();
359                                super::doc_elem_name(uri,None,title)
360                            }))
361                        )}}</div>
362                        <div>{if problems.is_empty() { None } else {Some(
363                            super::comma_sep("Problems", problems.into_iter().map(|(_,uri,cd)| {
364                                let title = uri.name().last_name().to_string();
365                                view!{
366                                    {super::doc_elem_name(uri,None,title)}
367                                    " ("{cd.to_string()}")"
368                                }
369                            }))
370                        )}}</div>
371                    }
372                })
373            }</div>
374        </LazyCollapsible>
375    }
376}
377
378#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
379#[cfg_attr(feature = "ts", derive(tsify_next::Tsify))]
380#[cfg_attr(feature = "ts", tsify(into_wasm_abi, from_wasm_abi))]
381pub struct OMDocSymbol {
382    pub uri: SymbolURI,
383    pub df: Option<Term>,
384    pub tp: Option<Term>,
385    pub arity: ArgSpec,
386    pub roles: Vec<String>,
387    pub macro_name: Option<String>,
388    //pub notations:Vec<(ModuleURI,String,Option<String>,Option<String>)>
389}
390impl super::OMDocT for OMDocSymbol {
391    fn into_view(self) -> impl IntoView {
392        let OMDocSymbol {
393            uri,
394            df,
395            tp,
396            arity,
397            roles,
398            macro_name,
399        } = self;
400        let show_separator = true; // !notations.is_empty();
401        let symbol_str = if use_context::<InStruct>().is_some() {
402            "Field "
403        } else if roles.iter().any(|s| s == "textsymdecl") {
404            "Text Symbol "
405        } else {
406            "Symbol "
407        };
408        let uriclone = uri.clone();
409        let uriclone_b = uri.clone();
410        view! {
411            <Block show_separator>
412                <Header slot><span>
413                    <b>{symbol_str}{super::symbol_name(&uri, uri.name().last_name().as_ref())}</b>
414                    {macro_name.map(|name| view!(<span>" ("<Text tag=TextTag::Code>"\\"{name}</Text>")"</span>))}
415                    {tp.map(|t| view! {
416                        " of type "{
417                            crate::remote::get!(present(t.clone()) = html => {
418                                view!(<FTMLStringMath html/>)
419                            })
420                        }
421                    })}
422                </span></Header>
423                <HeaderLeft slot>{do_notations(URI::Content(uriclone_b.into()),arity)}</HeaderLeft>
424                <HeaderRight slot><span style="white-space:nowrap;">{df.map(|t| view! {
425                    "Definiens: "{
426                        crate::remote::get!(present(t.clone()) = html => {
427                            view!(<FTMLStringMath html/>)
428                        })
429                    }
430                })}</span></HeaderRight>
431                {do_los(uriclone)}
432            </Block>
433        }
434    }
435}
436impl From<OMDocSymbol> for OMDoc {
437    #[inline]
438    fn from(value: OMDocSymbol) -> Self {
439        Self::SymbolDeclaration(value)
440    }
441}
442impl From<OMDocSymbol> for OMDocDeclaration {
443    #[inline]
444    fn from(value: OMDocSymbol) -> Self {
445        Self::Symbol(value)
446    }
447}
448
449#[cfg(feature = "ssr")]
450mod froms {
451    use super::{
452        super::OMDoc, OMDocDeclaration, OMDocExtension, OMDocModule, OMDocMorphism, OMDocStructure,
453        OMDocSymbol,
454    };
455    use flams_ontology::{
456        content::{
457            declarations::{
458                morphisms::Morphism,
459                structures::{Extension, MathStructure},
460                symbols::Symbol,
461                Declaration, OpenDeclaration,
462            },
463            modules::{Module, NestedModule},
464            ModuleLike, ModuleTrait,
465        },
466        uris::ModuleURI,
467        Checked, Resolvable,
468    };
469    use flams_system::backend::{Backend, StringPresenter};
470    use flams_utils::vecmap::VecSet;
471
472    impl OMDoc {
473        pub fn from_module_like<B: Backend>(
474            m: &ModuleLike,
475            backend: &B, //&mut StringPresenter<'_,B>
476        ) -> Self {
477            match m {
478                ModuleLike::Module(m) => OMDocModule::from_module(m, backend).into(),
479                ModuleLike::NestedModule(m) => {
480                    let mut imports = VecSet::new();
481                    let children =
482                        OMDocDeclaration::do_children(backend, &m.as_ref().elements, &mut imports);
483                    OMDocModule {
484                        uri: m.as_ref().uri.clone().into_module(),
485                        children,
486                        imports,
487                        uses: VecSet::new(),
488                        metatheory: None,
489                        signature: None,
490                    }
491                    .into()
492                }
493                ModuleLike::Structure(s) => {
494                    OMDocStructure::from_structure(s.as_ref(), backend).into()
495                }
496                ModuleLike::Extension(e) => {
497                    OMDocExtension::from_extension(e.as_ref(), backend).into()
498                }
499                ModuleLike::Morphism(m) => OMDocMorphism::from_morphism(m.as_ref(), backend).into(),
500            }
501        }
502    }
503
504    impl OMDocSymbol {
505        pub fn from_symbol<B: Backend>(
506            Symbol {
507                uri,
508                arity,
509                df,
510                tp,
511                macroname,
512                role,
513                ..
514            }: &Symbol,
515            backend: &B, //&mut StringPresenter<'_,B>,
516        ) -> Self {
517            Self {
518                uri: uri.clone(),
519                arity: arity.clone(),
520                roles: role.iter().map(|s| s.to_string()).collect(),
521                df: df.clone(), //.as_ref().and_then(|t| backend.present(t).ok()),
522                tp: tp.clone(), //.as_ref().and_then(|t| backend.present(t).ok()),
523                macro_name: macroname.as_ref().map(ToString::to_string),
524                //notations:Vec::new() // TODO
525            }
526        }
527    }
528
529    impl OMDocModule<OMDocDeclaration> {
530        pub fn from_module<B: Backend>(
531            module: &Module,
532            backend: &B, //&mut StringPresenter<'_,B>,
533        ) -> Self {
534            let uri = module.id().into_owned();
535            let metatheory = module.meta().map(|c| c.id().into_owned());
536            let signature = module.signature().map(|c| c.id().into_owned());
537            let mut imports = VecSet::new();
538            let children =
539                OMDocDeclaration::do_children(backend, module.declarations(), &mut imports);
540            Self {
541                uri,
542                metatheory,
543                signature,
544                children,
545                uses: VecSet::default(),
546                imports,
547            }
548        }
549    }
550
551    impl OMDocStructure<OMDocDeclaration> {
552        pub fn from_structure<B: Backend>(
553            s: &MathStructure<Checked>,
554            backend: &B, //&mut StringPresenter<'_,B>,
555        ) -> Self {
556            let uri = s.uri.clone();
557            let macro_name = s.macroname.as_ref().map(ToString::to_string);
558            let extensions = super::super::froms::get_extensions(backend, &uri)
559                .map(|e| {
560                    (
561                        e.as_ref().uri.clone(),
562                        e.as_ref()
563                            .elements
564                            .iter()
565                            .filter_map(|e| {
566                                if let OpenDeclaration::Symbol(s) = e {
567                                    Some(OMDocSymbol::from_symbol(s, backend))
568                                } else {
569                                    None
570                                }
571                            })
572                            .collect(),
573                    )
574                })
575                .collect();
576            let mut imports = VecSet::new();
577            let children = OMDocDeclaration::do_children(backend, s.declarations(), &mut imports);
578            Self {
579                uri,
580                macro_name,
581                extends: imports,
582                uses: VecSet::new(),
583                children,
584                extensions,
585            }
586        }
587    }
588
589    impl OMDocExtension<OMDocDeclaration> {
590        pub fn from_extension<B: Backend>(
591            e: &Extension<Checked>,
592            backend: &B, //&mut StringPresenter<'_,B>
593        ) -> Self {
594            let target = e.target.id().into_owned();
595            let uri = e.uri.clone();
596            let mut imports = VecSet::new();
597            let children = OMDocDeclaration::do_children(backend, &e.elements, &mut imports);
598            OMDocExtension {
599                uri,
600                target,
601                uses: VecSet::new(),
602                children,
603            }
604        }
605    }
606
607    impl OMDocMorphism<OMDocDeclaration> {
608        pub fn from_morphism<B: Backend>(
609            m: &Morphism<Checked>,
610            backend: &B, //&mut StringPresenter<'_,B>
611        ) -> Self {
612            let uri = m.uri.clone();
613            let total = m.total;
614            let target = Some(m.domain.id().into_owned());
615            let mut imports = VecSet::new();
616            let children = OMDocDeclaration::do_children(backend, &m.elements, &mut imports);
617            OMDocMorphism {
618                uri,
619                total,
620                target,
621                uses: VecSet::new(),
622                children,
623            }
624        }
625    }
626
627    impl OMDocDeclaration {
628        pub fn do_children<B: Backend>(
629            backend: &B, //&mut StringPresenter<'_,B>,
630            children: &[Declaration],
631            imports: &mut VecSet<ModuleURI>,
632        ) -> Vec<Self> {
633            let mut ret = Vec::new();
634            for c in children {
635                match c {
636                    OpenDeclaration::Symbol(s) => {
637                        ret.push(OMDocSymbol::from_symbol(s, backend).into())
638                    }
639                    OpenDeclaration::Import(m) => imports.insert(m.id().into_owned()),
640                    OpenDeclaration::MathStructure(s) => {
641                        ret.push(OMDocStructure::from_structure(s, backend).into())
642                    }
643                    OpenDeclaration::NestedModule(m) => {
644                        let mut imports = VecSet::new();
645                        let children = Self::do_children(backend, &m.elements, &mut imports);
646                        ret.push(
647                            OMDocModule {
648                                uri: m.uri.clone().into_module(),
649                                children,
650                                imports,
651                                uses: VecSet::new(),
652                                metatheory: None,
653                                signature: None,
654                            }
655                            .into(),
656                        )
657                    }
658                    OpenDeclaration::Extension(e) => {
659                        ret.push(OMDocExtension::from_extension(e, backend).into())
660                    }
661                    OpenDeclaration::Morphism(m) => {
662                        ret.push(OMDocMorphism::from_morphism(m, backend).into())
663                    }
664                }
665            }
666            ret
667        }
668    }
669}