89 lines
2.8 KiB
Rust
89 lines
2.8 KiB
Rust
|
use {
|
|||
|
|
r3vi::{
|
|||
|
|
view::{
|
|||
|
|
OuterViewPort,
|
|||
|
|
singleton::*,
|
|||
|
|
port::UpdateTask
|
|||
|
|
},
|
|||
|
|
buffer::singleton::*
|
|||
|
|
},
|
|||
|
|
laddertypes::{TypeTerm},
|
|||
|
|
crate::{
|
|||
|
|
repr_tree::{Context, ReprTree, ReprLeaf, ReprTreeExt, GenericReprTreeMorphism},
|
|||
|
|
edit_tree::{EditTree, TreeNavResult},
|
|||
|
|
editors::{
|
|||
|
|
char::CharEditor,
|
|||
|
|
ObjCommander
|
|||
|
|
},
|
|||
|
|
},
|
|||
|
|
std::sync::Arc,
|
|||
|
|
std::sync::RwLock
|
|||
|
|
};
|
|||
|
|
|
|||
|
|
pub fn init_ctx( ctx: Arc<RwLock<Context>> ) {
|
|||
|
|
|
|||
|
|
let char_morph_to_edittree = GenericReprTreeMorphism::new(
|
|||
|
|
Context::parse(&ctx, "Char"),
|
|||
|
|
Context::parse(&ctx, "Char~EditTree"),
|
|||
|
|
{
|
|||
|
|
let ctx = ctx.clone();
|
|||
|
|
move |rt, σ| {
|
|||
|
|
{
|
|||
|
|
let mut b = rt.write().unwrap().singleton_buffer::<char>();
|
|||
|
|
if let Some(buf) = b {
|
|||
|
|
// buffer already exists
|
|||
|
|
} else {
|
|||
|
|
// create char buffer
|
|||
|
|
rt.write().unwrap().insert_leaf(
|
|||
|
|
vec![].into_iter(),
|
|||
|
|
ReprLeaf::from_singleton_buffer(SingletonBuffer::new('\0'))
|
|||
|
|
);
|
|||
|
|
}
|
|||
|
|
}
|
|||
|
|
|
|||
|
|
let char_buf = rt.singleton_buffer::<char>();
|
|||
|
|
let mut edittree = CharEditor::new_edit_tree(
|
|||
|
|
ctx.clone(),
|
|||
|
|
char_buf,
|
|||
|
|
SingletonBuffer::<usize>::new(0).get_port()
|
|||
|
|
);
|
|||
|
|
|
|||
|
|
rt.insert_leaf(
|
|||
|
|
Context::parse(&ctx, "EditTree"),
|
|||
|
|
ReprLeaf::from_singleton_buffer(
|
|||
|
|
SingletonBuffer::new(
|
|||
|
|
Arc::new(RwLock::new(edittree))
|
|||
|
|
)
|
|||
|
|
)
|
|||
|
|
);
|
|||
|
|
|
|||
|
|
ctx.read().unwrap().setup_edittree(rt);
|
|||
|
|
}
|
|||
|
|
}
|
|||
|
|
);
|
|||
|
|
|
|||
|
|
let char_morph_from_edittree = GenericReprTreeMorphism::new(
|
|||
|
|
Context::parse(&ctx, "Char~EditTree"),
|
|||
|
|
Context::parse(&ctx, "Char"),
|
|||
|
|
{
|
|||
|
|
let ctx = ctx.clone();
|
|||
|
|
move |rt, σ|
|
|||
|
|
{
|
|||
|
|
let mut b = rt
|
|||
|
|
.descend(Context::parse(&ctx, "EditTree")).unwrap()
|
|||
|
|
.view_singleton::<Arc<RwLock<EditTree>>>();
|
|||
|
|
|
|||
|
|
rt.attach_leaf_to(
|
|||
|
|
Context::parse(&ctx, "Char"),
|
|||
|
|
b.map(|x|
|
|||
|
|
x.read().unwrap()
|
|||
|
|
.get_edit::<CharEditor>().unwrap()
|
|||
|
|
.read().unwrap()
|
|||
|
|
.get())
|
|||
|
|
);
|
|||
|
|
}
|
|||
|
|
});
|
|||
|
|
ctx.write().unwrap().morphisms.add_morphism( char_morph_to_edittree );
|
|||
|
|
ctx.write().unwrap().morphisms.add_morphism( char_morph_from_edittree );
|
|||
|
|
}
|