Skip to content

Commit 4107cd3

Browse files
committed
Implement correct scroll bar behaviour for param history
1 parent c004e76 commit 4107cd3

File tree

2 files changed

+11
-11
lines changed

2 files changed

+11
-11
lines changed

src/ui/panel/Panel.re

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -40,18 +40,20 @@ let make = (~state, ~dispatch) => {
4040

4141
let locations = (state.goblint)#dead_locations;
4242

43+
let panel = switch (current) {
44+
| Some(Warnings) => <WarningView warnings={state.warnings} dispatch />
45+
| Some(DeadCode) => <DeadCodeView locations dispatch />
46+
| Some(Parameters) => <ParameterView parameters />
47+
| Some(Statistics) => <GvStatisticsView stats={state.stats} />
48+
| _ => React.null
49+
};
50+
4351
let current = state.selected_panel;
4452
<div className="panel d-flex flex-column border-right border-left h-25">
4553
{make_nav_pills(current, dispatch)}
4654
<div className="tab-content overflow-auto">
4755
<div className="tab-pane active">
48-
{switch (current) {
49-
| Some(Warnings) => <WarningView warnings={state.warnings} dispatch />
50-
| Some(DeadCode) => <DeadCodeView locations dispatch />
51-
| Some(Parameters) => <ParameterView parameters />
52-
| Some(Statistics) => <GvStatisticsView stats={state.stats} />
53-
| _ => React.null
54-
}}
56+
{panel}
5557
</div>
5658
</div>
5759
</div>;

src/ui/panel/ParameterView.re

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,6 @@ let make = (~parameters) => {
4343
};
4444

4545
<div>
46-
//<div className="d-flex justify-content-between">
47-
//</div>
4846
<div className="input-group">
4947
<Button on_click={on_submit}>
5048
<IconPlay fill="bi bi-play-fill" />
@@ -55,11 +53,11 @@ let make = (~parameters) => {
5553
</Button>
5654
<Input value on_change on_submit />
5755
</div>
58-
<div className="container-fluid text-center" style={ReactDOM.Style.make(~height="120px", ())}>
56+
<div className="container-fluid text-center">
5957
<div className="row align-items-center">
6058
{"History" |> React.string}
6159
</div>
62-
<div className="row">
60+
<div className="row" style={ReactDOM.Style.make(~height="120px", ~maxHeight="100%", ~overflow="auto", ())}>
6361
<ol key={"params_list"} className="list-group">
6462
{list_elements |> Array.to_list |> React.list}
6563
</ol>

0 commit comments

Comments
 (0)