machine-check-gui 0.7.1

Utility crate for the formal verification tool machine-check
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77

use wasm_bindgen::JsCast;

use crate::frontend::{
    client::{render, view_singleton::lock_view},
    util::web_idl::setup_selector_listener,
    view::NavigationTarget,
};

#[derive(Clone, Copy, Debug)]
pub enum KeyboardEvent {
    Down,
    Up,
}

mod codes {
    pub const HOME: &str = "Home";
    pub const ARROW_UP: &str = "ArrowUp";
    pub const ARROW_LEFT: &str = "ArrowLeft";
    pub const ARROW_RIGHT: &str = "ArrowRight";
    pub const ARROW_DOWN: &str = "ArrowDown";
}

pub fn init() {
    for (event_type, event_name) in [
        (KeyboardEvent::Down, "keydown"),
        (KeyboardEvent::Up, "keyup"),
    ] {
        setup_selector_listener(
            "#main_area",
            event_name,
            Box::new(move |e| {
                wasm_bindgen_futures::spawn_local(on_keyboard(event_type, e));
            }),
        );
        setup_selector_listener(
            "#main_canvas",
            event_name,
            Box::new(move |e| {
                wasm_bindgen_futures::spawn_local(on_keyboard(event_type, e));
            }),
        );
    }
}

async fn on_keyboard(keyboard: KeyboardEvent, event: web_sys::Event) {
    let mut view_guard = lock_view();
    let view = view_guard.as_mut();
    console_log!("Keyboard event received: {:?}", event);

    let event: web_sys::KeyboardEvent = event
        .dyn_into()
        .expect("Keyboard event should be KeyboardEvent");

    let navigation_target = match event.code().as_str() {
        codes::HOME => NavigationTarget::Root,
        codes::ARROW_UP => NavigationTarget::Up,
        codes::ARROW_DOWN => NavigationTarget::Down,
        codes::ARROW_LEFT => NavigationTarget::Left,
        codes::ARROW_RIGHT => NavigationTarget::Right,
        _ => return,
    };

    // prevent default action only for the handled events
    // to prevent keyboard traps
    event.prevent_default();

    match keyboard {
        KeyboardEvent::Down => {
            view.navigate(navigation_target);
            // redraw
            render(view);
        }
        KeyboardEvent::Up => {
            // nothing for now
        }
    }
}