Skip to content

Commit

Permalink
revert attempted (failed) bug fix
Browse files Browse the repository at this point in the history
  • Loading branch information
caileans committed Apr 23, 2024
1 parent 64988e8 commit 27fbab1
Show file tree
Hide file tree
Showing 3 changed files with 5 additions and 5 deletions.
2 changes: 1 addition & 1 deletion web-app/src/components/expr_entry.rs
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ impl ExprEntry {
let cursor_pos = left.chars().count() as u32;

// Update text field value
let value = [[left, right].concat(), " ".to_string()].concat();
let value = [left, right].concat();
input_elem.set_value(&value);

// Update cursor position
Expand Down
7 changes: 3 additions & 4 deletions web-app/src/components/proof_widget/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -179,10 +179,9 @@ impl ProofWidget {
//tooltip portion addapted from:
// * https://stackoverflow.com/questions/31483302/how-to-display-an-image-inside-bootstrap-tooltip
// * https://getbootstrap.com/docs/4.1/components/tooltips/

html! {
<button class="dropdown-item" type="button" data-toggle="tooltip" data-placement="right" title={format!("<img id='rule-img' src='proofImages_light/{}.png' width=100% border-radius:4px/>", rule.get_name())} onclick={ ctx.link().callback(move |_| ProofWidgetMsg::LineAction(LineActionKind::SetRule { rule }, pjref)) }>
{ rule.get_name() }
html! {
<button class="dropdown-item" type="button" data-toggle="tooltip" data-placement="right" title={format!("<img id='rule-img' src='proofImages_light/{}.png'/>", rule.get_name())} onclick={ ctx.link().callback(move |_| ProofWidgetMsg::LineAction(LineActionKind::SetRule { rule }, pjref)) }>
{ rule.get_name() }
</button>
}
})
Expand Down
1 change: 1 addition & 0 deletions web-app/static/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@
// * https://stackoverflow.com/questions/31483302/how-to-display-an-image-inside-bootstrap-tooltip
// * https://stackoverflow.com/questions/24655291/how-to-bind-bootstrap-tooltip-on-dynamic-elements
$('body').tooltip({ selector: '[data-toggle="tooltip"]', html:true});

</script>
</body>

Expand Down

0 comments on commit 27fbab1

Please sign in to comment.