|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// Example: Using SafeDOM for formally verified DOM mounting |
| 3 | + |
| 4 | +import SafeDOM |
| 5 | + |
| 6 | +// Example 1: Basic mounting with error handling |
| 7 | +fn mount_app() { |
| 8 | + SafeDOM::mount_safe( |
| 9 | + "#app", |
| 10 | + "<div><h1>Hello, World!</h1><p>Mounted safely with proofs.</p></div>", |
| 11 | + on_success: fn(el) { |
| 12 | + Console::log("✓ App mounted successfully!") |
| 13 | + Console::log("Element: ", el) |
| 14 | + }, |
| 15 | + on_error: fn(err) { |
| 16 | + Console::error("✗ Mount failed: ", err) |
| 17 | + } |
| 18 | + ) |
| 19 | +} |
| 20 | + |
| 21 | +// Example 2: Wait for DOM ready before mounting |
| 22 | +fn mount_when_dom_ready() { |
| 23 | + SafeDOM::mount_when_ready( |
| 24 | + "#app", |
| 25 | + "<div class='container'><h1>App Title</h1></div>", |
| 26 | + on_success: fn(_) { Console::log("✓ Mounted after DOM ready") }, |
| 27 | + on_error: fn(err) { Console::error("✗ Failed: ", err) } |
| 28 | + ) |
| 29 | +} |
| 30 | + |
| 31 | +// Example 3: Batch mounting (atomic - all or nothing) |
| 32 | +fn mount_multiple() { |
| 33 | + let specs = [ |
| 34 | + {selector: "#header", html: "<header><h1>Site Title</h1></header>"}, |
| 35 | + {selector: "#nav", html: "<nav><a href='/'>Home</a></nav>"}, |
| 36 | + {selector: "#main", html: "<main><p>Content here</p></main>"}, |
| 37 | + {selector: "#footer", html: "<footer>© 2026</footer>"} |
| 38 | + ] |
| 39 | + |
| 40 | + match SafeDOM::mount_batch(specs) { |
| 41 | + Ok(elements) => { |
| 42 | + Console::log("✓ Successfully mounted ", len(elements), " elements") |
| 43 | + for el in elements { |
| 44 | + Console::log(" -", el) |
| 45 | + } |
| 46 | + } |
| 47 | + Error(err) => { |
| 48 | + Console::error("✗ Batch mount failed: ", err) |
| 49 | + Console::error(" (None were mounted - atomic operation)") |
| 50 | + } |
| 51 | + } |
| 52 | +} |
| 53 | + |
| 54 | +// Example 4: Explicit validation before mounting |
| 55 | +fn mount_with_validation() { |
| 56 | + // Validate selector first |
| 57 | + match ProvenSelector::validate("#my-app") { |
| 58 | + Error(e) => Console::error("Invalid selector: ", e) |
| 59 | + Ok(valid_selector) => { |
| 60 | + // Validate HTML |
| 61 | + match ProvenHTML::validate("<div>Content</div>") { |
| 62 | + Error(e) => Console::error("Invalid HTML: ", e) |
| 63 | + Ok(valid_html) => { |
| 64 | + // Now mount with proven safety |
| 65 | + match SafeDOM::mount(valid_selector, valid_html) { |
| 66 | + Mounted(el) => Console::log("✓ Mounted with validated inputs: ", el) |
| 67 | + MountPointNotFound(s) => Console::error("✗ Element not found: ", s) |
| 68 | + InvalidSelector(_) => Console::error("Impossible - already validated") |
| 69 | + InvalidHTML(_) => Console::error("Impossible - already validated") |
| 70 | + } |
| 71 | + } |
| 72 | + } |
| 73 | + } |
| 74 | + } |
| 75 | +} |
| 76 | + |
| 77 | +// Example 5: Integration with TEA |
| 78 | +namespace MyApp { |
| 79 | + struct Model { |
| 80 | + message: String |
| 81 | + } |
| 82 | + |
| 83 | + enum Msg { |
| 84 | + NoOp |
| 85 | + } |
| 86 | + |
| 87 | + fn init() -> Model { |
| 88 | + Model{message: "Hello from TEA"} |
| 89 | + } |
| 90 | + |
| 91 | + fn update(_model: Model, _msg: Msg) -> Model { |
| 92 | + _model |
| 93 | + } |
| 94 | + |
| 95 | + fn view(model: Model) -> String { |
| 96 | + "<div><h1>" + model.message + "</h1></div>" |
| 97 | + } |
| 98 | +} |
| 99 | + |
| 100 | +fn mount_tea_app() { |
| 101 | + let model = MyApp::init() |
| 102 | + let html = MyApp::view(model) |
| 103 | + |
| 104 | + SafeDOM::mount_when_ready( |
| 105 | + "#tea-app", |
| 106 | + html, |
| 107 | + on_success: fn(el) { |
| 108 | + Console::log("✓ TEA app mounted") |
| 109 | + // Set up event handlers, subscriptions here |
| 110 | + }, |
| 111 | + on_error: fn(err) { Console::error("✗ TEA mount failed: ", err) } |
| 112 | + ) |
| 113 | +} |
| 114 | + |
| 115 | +// Entry point |
| 116 | +fn main() { |
| 117 | + Console::log("SafeDOM Examples") |
| 118 | + Console::log("================\n") |
| 119 | + |
| 120 | + // Choose which example to run |
| 121 | + mount_when_dom_ready() // Run on DOM ready |
| 122 | +} |
| 123 | + |
| 124 | +// Auto-execute when module loads |
| 125 | +main() |
0 commit comments