Skip to content
Snippets Groups Projects
Commit 43d876f0 authored by David Bühler's avatar David Bühler
Browse files

[ivette] Adds a fixed tiny space at the end of component titlebars.

parent e1fa9dce
No related branches found
No related tags found
No related merge requests found
...@@ -29,7 +29,6 @@ import * as Utils from 'dome/data/arrays'; ...@@ -29,7 +29,6 @@ import * as Utils from 'dome/data/arrays';
import * as States from 'frama-c/states'; import * as States from 'frama-c/states';
import * as Settings from 'dome/data/settings'; import * as Settings from 'dome/data/settings';
import { IconButton } from 'dome/controls/buttons'; import { IconButton } from 'dome/controls/buttons';
import { Filler, Inset } from 'dome/frame/toolbars';
import * as Studia from 'frama-c/plugins/studia'; import * as Studia from 'frama-c/plugins/studia';
import * as Ast from 'frama-c/kernel/api/ast'; import * as Ast from 'frama-c/kernel/api/ast';
import { text } from 'frama-c/kernel/api/data'; import { text } from 'frama-c/kernel/api/data';
...@@ -739,14 +738,12 @@ export default function ASTview(): JSX.Element { ...@@ -739,14 +738,12 @@ export default function ASTview(): JSX.Element {
return ( return (
<> <>
<TitleBar> <TitleBar>
<Filler />
<IconButton <IconButton
icon={icon} icon={icon}
onClick= {unFoldButtonClicked} onClick= {unFoldButtonClicked}
title={title + ' all multi-line ACSL properties'} title={title + ' all multi-line ACSL properties'}
className="titlebar-thin-icon" className="titlebar-thin-icon"
/> />
<Inset />
</TitleBar> </TitleBar>
<Component style={{ fontSize: `${fontSize}px` }} /> <Component style={{ fontSize: `${fontSize}px` }} />
</> </>
......
...@@ -33,6 +33,7 @@ import React from 'react'; ...@@ -33,6 +33,7 @@ import React from 'react';
import { DEVEL } from 'dome'; import { DEVEL } from 'dome';
import { Label } from 'dome/controls/labels'; import { Label } from 'dome/controls/labels';
import { DefineElement } from 'dome/layout/dispatch'; import { DefineElement } from 'dome/layout/dispatch';
import { Inset } from 'dome/frame/toolbars';
import * as State from './state'; import * as State from './state';
import * as Search from './search'; import * as Search from './search';
...@@ -191,6 +192,7 @@ export function TitleBar(props: TitleBarProps): JSX.Element | null { ...@@ -191,6 +192,7 @@ export function TitleBar(props: TitleBarProps): JSX.Element | null {
title={title || context.title} title={title || context.title}
/> />
{children} {children}
<Inset />
</DefineElement> </DefineElement>
); );
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment