diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index 3ee22ca3abb820bf1edb0450e028709f9184733b..9f815c5f29abce999d9cb73c4867225e86a4f3d9 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -8,13 +8,14 @@ import * as Dome from 'dome';
 import * as Json from 'dome/data/json';
 import * as States from 'frama-c/states';
 import * as Compare from 'dome/data/compare';
+import * as Settings from 'dome/data/settings';
 import { Label, Code } from 'dome/controls/labels';
 import { IconButton, Checkbox } from 'dome/controls/buttons';
 import * as Models from 'dome/table/models';
 import * as Arrays from 'dome/table/arrays';
 import { Table, Column, ColumnProps, Renderer } from 'dome/table/views';
 import { TitleBar, Component } from 'frama-c/LabViews';
-import { Vfill, Folder } from 'dome/layout/boxes';
+import { Scroll, Folder } from 'dome/layout/boxes';
 
 import { RSplit } from 'dome/layout/splitters';
 
@@ -26,141 +27,151 @@ import * as Properties from 'api/kernel/properties';
 // --- Filters
 // --------------------------------------------------------------------------
 
-const defaultStatusFilter =
-{
-  valid: true,
-  valid_hyp: true,
-  unknown: true,
-  invalid: true,
-  invalid_hyp: true,
-  considered_valid: false,
-  untried: false,
-  inconsistent: true,
-};
-
-const defaultKindFilter =
-{
-  assert: true,
-  invariant: true,
-  variant: true,
-  requires: true,
-  ensures: true,
-  instance: true,
-  assumes: true,
-  assigns: true,
-  from: true,
-  allocates: true,
-  behavior: false,
-  reachable: false,
-  axiomatic: true,
-  pragma: true,
-  others: true,
+const DEFAULTS: { [key: string]: boolean } = {
+  currentFunction: false,
+  'status.valid': true,
+  'status.valid_hyp': true,
+  'status.unknown': true,
+  'status.invalid': true,
+  'status.invalid_hyp': true,
+  'status.considered_valid': false,
+  'status.untried': false,
+  'status.inconsistent': true,
+  'kind.assert': true,
+  'kind.invariant': true,
+  'kind.variant': true,
+  'kind.requires': true,
+  'kind.ensures': true,
+  'kind.instance': true,
+  'kind.assumes': true,
+  'kind.assigns': true,
+  'kind.froms': true,
+  'kind.allocates': true,
+  'kind.behavior': false,
+  'kind.reachable': false,
+  'kind.axiomatic': true,
+  'kind.pragma': true,
+  'kind.others': true,
+  'alarms.alarms': true, // show properties that are alarms
+  'alarms.others': true, // show properties that are not alarms
+  'alarms.overflow': true,
+  'alarms.division_by_zero': true,
+  'alarms.mem_access': true,
+  'alarms.index_bound': true,
+  'alarms.pointer_value': true,
+  'alarms.shift': true,
+  'alarms.ptr_comparison': true,
+  'alarms.differing_blocks': true,
+  'alarms.separation': true,
+  'alarms.overlap': true,
+  'alarms.initialization': true,
+  'alarms.dangling_pointer': true,
+  'alarms.special_float': true,
+  'alarms.float_to_int': true,
+  'alarms.function_pointer': true,
+  'alarms.union_initialization': true,
+  'alarms.bool_value': true,
 };
 
-const defaultAlarmsFilter =
-{
-  alarms: true, // show properties that are alarms
-  others: true, // show properties that are not alarms
-  overflow: true,
-  division_by_zero: true,
-  mem_access: true,
-  index_bound: true,
-  pointer_value: true,
-  shift: true,
-  ptr_comparison: true,
-  differing_blocks: true,
-  separation: true,
-  overlap: true,
-  initialization: true,
-  dangling_pointer: true,
-  special_float: true,
-  float_to_int: true,
-  function_pointer: true,
-  union_initialization: true,
-  bool_value: true,
-};
+function filter(path: string) {
+  const defaultValue = DEFAULTS[path] ?? true;
+  return Settings.getWindowSettings(
+    `ivette.properties.filter.${path}`,
+    Json.jBoolean,
+    defaultValue,
+  );
+}
 
-const defaultFilter =
-{
-  currentFunction: false,
-  status: defaultStatusFilter,
-  kind: defaultKindFilter,
-  alarms: defaultAlarmsFilter,
-};
+function useFilter(path: string) {
+  const defaultValue = DEFAULTS[path] ?? true;
+  return Dome.useFlipSettings(
+    `ivette.properties.filter.${path}`,
+    defaultValue,
+  );
+}
 
 function filterStatus(
-  f: typeof defaultStatusFilter,
   status: Properties.propStatus,
 ) {
   switch (status) {
     case 'valid':
-    case 'valid_but_dead': return f.valid;
-    case 'valid_under_hyp': return f.valid_hyp;
+    case 'valid_but_dead':
+      return filter('status.valid');
+    case 'valid_under_hyp':
+      return filter('status.valid_hyp');
     case 'invalid':
-    case 'invalid_but_dead': return f.invalid;
-    case 'invalid_under_hyp': return f.invalid_hyp;
+    case 'invalid_but_dead':
+      return filter('status.invalid');
+    case 'invalid_under_hyp':
+      return filter('status.invalid_hyp');
+    case 'inconsistent':
+      return filter('inconsistent');
     case 'unknown':
-    case 'unknown_but_dead': return f.unknown;
-    case 'considered_valid': return f.considered_valid;
-    case 'never_tried': return f.untried;
-    case 'inconsistent': return f.inconsistent;
-    default: return true;
+    case 'unknown_but_dead':
+      return filter('status.unknown');
+    case 'considered_valid':
+      return filter('considered_valid');
+    case 'never_tried':
+      return filter('status.untried');
+    default:
+      return true;
   }
 }
 
 function filterKind(
-  f: typeof defaultKindFilter,
   kind: Properties.propKind,
 ) {
   switch (kind) {
-    case 'assert': return f.assert;
-    case 'loop_invariant':
-      return f.invariant;
-    case 'loop_variant': return f.variant;
-    case 'requires': return f.requires;
-    case 'ensures': return f.ensures;
-    case 'instance': return f.instance;
-    case 'assigns': return f.assigns;
-    case 'froms': return f.from;
-    case 'allocates': return f.allocates;
-    case 'behavior': return f.behavior;
-    case 'reachable': return f.reachable;
-    case 'axiomatic': return f.axiomatic;
-    case 'loop_pragma': return f.pragma;
-    default: return f.others;
+    case 'assert': return filter('kind.assert');
+    case 'loop_invariant': return filter('kind.invariant');
+    case 'loop_variant': return filter('kind.variant');
+    case 'requires': return filter('kind.requires');
+    case 'ensures': return filter('kind.ensures');
+    case 'instance': return filter('kind.instance');
+    case 'assigns': return filter('kind.assigns');
+    case 'froms': return filter('kind.froms');
+    case 'allocates': return filter('kind.allocates');
+    case 'behavior': return filter('kind.behavior');
+    case 'reachable': return filter('kind.reachable');
+    case 'axiomatic': return filter('kind.axiomatic');
+    case 'loop_pragma': return filter('kind.pragma');
+    default: return filter('kind.others');
   }
 }
 
-function filterAlarm(f: typeof defaultAlarmsFilter, alarm: string) {
-  switch (alarm) {
-    case 'overflow': return f.overflow;
-    case 'division_by_zero': return f.division_by_zero;
-    case 'mem_access': return f.mem_access;
-    case 'index_bound': return f.index_bound;
-    case 'pointer_value': return f.pointer_value;
-    case 'shift': return f.shift;
-    case 'ptr_comparison': return f.ptr_comparison;
-    case 'differing_blocks': return f.differing_blocks;
-    case 'separation': return f.separation;
-    case 'overlap': return f.overlap;
-    case 'initialization': return f.initialization;
-    case 'dangling_pointer': return f.dangling_pointer;
-    case 'is_nan_or_infinite':
-    case 'is_nan': return f.special_float;
-    case 'float_to_int': return f.float_to_int;
-    case 'function_pointer': return f.function_pointer;
-    case 'initialization_of_union': return f.union_initialization;
-    case 'bool_value': return f.bool_value;
-    default: return true;
+function filterAlarm(alarm: string | undefined) {
+  if (alarm) {
+    if (!filter('alarms.alarms')) return false;
+    switch (alarm) {
+      case 'overflow': return filter('alarms.overflow');
+      case 'division_by_zero': return filter('alarms.division_by_zero');
+      case 'mem_access': return filter('alarms.mem_access');
+      case 'index_bound': return filter('alarms.index_bound');
+      case 'pointer_value': return filter('alarms.pointer_value');
+      case 'shift': return filter('alarms.shift');
+      case 'ptr_comparison': return filter('alarms.ptr_comparison');
+      case 'differing_blocks': return filter('alarms.differing_blocks');
+      case 'separation': return filter('alarms.separation');
+      case 'overlap': return filter('alarms.overlap');
+      case 'initialization': return filter('alarms.initialization');
+      case 'dangling_pointer': return filter('alarms.dangling_pointer');
+      case 'is_nan_or_infinite':
+      case 'is_nan': return filter('alarms.special_float');
+      case 'float_to_int': return filter('alarms.float_to_int');
+      case 'function_pointer': return filter('alarms.function_pointer');
+      case 'initialization_of_union':
+        return filter('alarms.union_initialization');
+      case 'bool_value': return filter('alarms.bool_value');
+      default: return false;
+    }
   }
+  return filter('alarms.others');
 }
 
-function filterProperty(f: typeof defaultFilter, item: Property) {
-  return filterStatus(f.status, item.status)
-    && filterKind(f.kind, item.kind)
-    && ((item.alarm && f.alarms.alarms)
-      || (!item.alarm && f.alarms.others))
-    && (!item.alarm || filterAlarm(f.alarms, item.alarm));
+function filterProperty(p: Property) {
+  return filterStatus(p.status)
+    && filterKind(p.kind)
+    && filterAlarm(p.alarm);
 }
 
 // --------------------------------------------------------------------------
@@ -242,7 +253,6 @@ const byColumn: Arrays.ByColumns<Property> = {
 class PropertyModel extends Arrays.CompactModel<Json.key<'#status'>, Property> {
 
   private filterFun?: string;
-  private filterProp = _.cloneDeep(defaultFilter);
 
   constructor() {
     super((p: Property) => p.key);
@@ -251,23 +261,17 @@ class PropertyModel extends Arrays.CompactModel<Json.key<'#status'>, Property> {
     this.setFilter(this.filterItem.bind(this));
   }
 
-  getFilterProps() {
-    return this.filterProp;
-  }
-
   setFilterFunction(kf?: string) {
     this.filterFun = kf;
-    if (this.filterProp.currentFunction)
-      this.reload();
+    if (filter('currentFunction')) this.reload();
   }
 
-  filterItem(item: Property) {
+  filterItem(prop: Property) {
+    const kf = prop.function;
     const cf = this.filterFun;
-    const cp = this.filterProp;
-    return (
-      (!cp.currentFunction || cf === undefined || cf === item.function) &&
-      filterProperty(cp, item)
-    );
+    const filteringFun = cf && filter('currentFunction');
+    const filterFunction = filteringFun ? kf === cf : true;
+    return filterFunction && filterProperty(prop);
   }
 
 }
@@ -276,7 +280,7 @@ class PropertyModel extends Arrays.CompactModel<Json.key<'#status'>, Property> {
 // --- Property Filter Form
 // -------------------------------------------------------------------------
 
-type BoolFields = { [key: string]: boolean };
+const MODEL = React.createContext(() => { });
 
 interface SectionProps {
   label: string;
@@ -285,7 +289,7 @@ interface SectionProps {
 }
 
 function Section(props: SectionProps) {
-  const settings = `propfilter-${props.path}`;
+  const settings = `properties-section-${props.path}`;
   return (
     <Folder label={props.label} settings={settings}>
       {props.children}
@@ -293,104 +297,81 @@ function Section(props: SectionProps) {
   );
 }
 
-interface CheckFieldProps<A, K extends keyof A> {
-  filter: A;
-  onChange: () => void;
+interface CheckFieldProps {
   label: string;
-  path: K;
+  path: string;
 }
 
-function CheckField<A extends BoolFields, K extends keyof A>(
-  props: CheckFieldProps<A, K>,
-) {
-  const forceUpdate = Dome.useForceUpdate();
-  const { label, filter, path, onChange } = props;
-  const update = (v: boolean) => {
-    (filter as any)[path] = v;
-    forceUpdate();
-    onChange();
-  };
+function CheckField(props: CheckFieldProps) {
+  const reload = React.useContext(MODEL);
+  const [value, setValue] = useFilter(props.path);
+  const onChange = () => { setValue(); reload(); };
   return (
     <Checkbox
       style={{ display: 'block' }}
-      label={label}
-      value={filter[path]}
-      onChange={update}
+      label={props.label}
+      value={value}
+      onChange={onChange}
     />
   );
 }
 
 /* eslint-disable max-len */
 
-function PropertyFilter(props: { model: PropertyModel }) {
-  const onChange = props.model.reload;
-  const filter = props.model.getFilterProps();
-  const setCurrentFunction = React.useCallback(
-    (v: boolean) => {
-      filter.currentFunction = v;
-      onChange();
-    }, [filter, onChange],
-  );
-  const status = { filter: filter.status, onChange };
-  const kind = { filter: filter.kind, onChange };
-  const alarms = { filter: filter.alarms, onChange };
+function PropertyFilter() {
   return (
-    <Vfill>
-      <Checkbox
-        label="Current function"
-        value={filter.currentFunction}
-        onChange={setCurrentFunction}
-      />
+    <Scroll>
+      <CheckField label="Current function" path="currentFunction" />
       <Section label="Status" path="status">
-        <CheckField {...status} label="Valid" path="valid" />
-        <CheckField {...status} label="Valid under hyp." path="valid_hyp" />
-        <CheckField {...status} label="Unknown" path="unknown" />
-        <CheckField {...status} label="Invalid" path="invalid" />
-        <CheckField {...status} label="Invalid under hyp." path="invalid_hyp" />
-        <CheckField {...status} label="Considered valid" path="considered_valid" />
-        <CheckField {...status} label="Untried" path="untried" />
-        <CheckField {...status} label="Inconsistent" path="inconsistent" />
+        <CheckField label="Valid" path="status.valid" />
+        <CheckField label="Valid under hyp." path="status.valid_hyp" />
+        <CheckField label="Unknown" path="status.unknown" />
+        <CheckField label="Invalid" path="status.invalid" />
+        <CheckField label="Invalid under hyp." path="status.invalid_hyp" />
+        <CheckField label="Considered valid" path="status.considered_valid" />
+        <CheckField label="Untried" path="status.untried" />
+        <CheckField label="Inconsistent" path="status.inconsistent" />
       </Section>
       <Section label="Property kind" path="kind">
-        <CheckField {...kind} label="Assertions" path="assert" />
-        <CheckField {...kind} label="Invariants" path="invariant" />
-        <CheckField {...kind} label="Variants" path="variant" />
-        <CheckField {...kind} label="Preconditions" path="requires" />
-        <CheckField {...kind} label="Postconditions" path="ensures" />
-        <CheckField {...kind} label="Instance" path="instance" />
-        <CheckField {...kind} label="Assigns clauses" path="assigns" />
-        <CheckField {...kind} label="From clauses" path="from" />
-        <CheckField {...kind} label="Allocates" path="allocates" />
-        <CheckField {...kind} label="Behaviors" path="behavior" />
-        <CheckField {...kind} label="Reachables" path="reachable" />
-        <CheckField {...kind} label="Axiomatics" path="axiomatic" />
-        <CheckField {...kind} label="Pragma" path="pragma" />
-        <CheckField {...kind} label="Others" path="others" />
+        <CheckField label="Assertions" path="kind.assert" />
+        <CheckField label="Invariants" path="kind.invariant" />
+        <CheckField label="Variants" path="kind.variant" />
+        <CheckField label="Preconditions" path="kind.requires" />
+        <CheckField label="Postconditions" path="kind.ensures" />
+        <CheckField label="Instance" path="kind.instance" />
+        <CheckField label="Assigns clauses" path="kind.assigns" />
+        <CheckField label="From clauses" path="kind.from" />
+        <CheckField label="Allocates" path="kind.allocates" />
+        <CheckField label="Behaviors" path="kind.behavior" />
+        <CheckField label="Reachables" path="kind.reachable" />
+        <CheckField label="Axiomatics" path="kind.axiomatic" />
+        <CheckField label="Pragma" path="kind.pragma" />
+        <CheckField label="Others" path="kind.others" />
       </Section>
       <Section label="Alarms" path="alarms">
-        <CheckField {...alarms} label="Alarms" path="alarms" />
-        <CheckField {...alarms} label="Others" path="others" />
+        <CheckField label="Alarms" path="alarms.alarms" />
+        <CheckField label="Others" path="alarms.others" />
       </Section>
       <Section label="Alarms kind" path="alarms">
-        <CheckField {...alarms} label="Overflows" path="overflow" />
-        <CheckField {...alarms} label="Divisions by zero" path="division_by_zero" />
-        <CheckField {...alarms} label="Shifts" path="shift" />
-        <CheckField {...alarms} label="Special floats" path="special_float" />
-        <CheckField {...alarms} label="Float to int" path="float_to_int" />
-        <CheckField {...alarms} label="_Bool values" path="bool_value" />
-        <CheckField {...alarms} label="Memory accesses" path="mem_access" />
-        <CheckField {...alarms} label="Index bounds" path="index_bound" />
-        <CheckField {...alarms} label="Initializations" path="initialization" />
-        <CheckField {...alarms} label="Dangling pointers" path="dangling_pointer" />
-        <CheckField {...alarms} label="Pointer values" path="pointer_value" />
-        <CheckField {...alarms} label="Function pointers" path="function_pointer" />
-        <CheckField {...alarms} label="Pointer comparisons" path="ptr_comparison" />
-        <CheckField {...alarms} label="Differing blocks" path="differing_blocks" />
-        <CheckField {...alarms} label="Separations" path="separation" />
-        <CheckField {...alarms} label="Overlaps" path="overlap" />
-        <CheckField {...alarms} label="Initialization of unions" path="union_initialization" />
+        <CheckField label="Overflows" path="alarms.overflow" />
+        <CheckField label="Divisions by zero" path="alarms.division_by_zero" />
+        <CheckField label="Shifts" path="alarms.shift" />
+        <CheckField label="Special floats" path="alarms.special_float" />
+        <CheckField label="Float to int" path="alarms.float_to_int" />
+        <CheckField label="_Bool values" path="alarms.bool_value" />
+        <CheckField label="Memory accesses" path="alarms.mem_access" />
+        <CheckField label="Index bounds" path="alarms.index_bound" />
+        <CheckField label="Initializations" path="alarms.initialization" />
+        <CheckField label="Dangling pointers" path="alarms.dangling_pointer" />
+        <CheckField label="Pointer values" path="alarms.pointer_value" />
+        <CheckField label="Function pointers" path="alarms.function_pointer" />
+        <CheckField label="Pointer comparisons" path="alarms.ptr_comparison" />
+        <CheckField label="Differing blocks" path="alarms.differing_blocks" />
+        <CheckField label="Separations" path="alarms.separation" />
+        <CheckField label="Overlaps" path="alarms.overlap" />
+        <CheckField label="Initialization of unions" path="alarms.union_initialization" />
       </Section>
-    </Vfill>
+    </Scroll>
   );
 }
 
@@ -540,7 +521,9 @@ const RenderTable = () => {
         >
           <PropertyColumns />
         </Table>
-        <PropertyFilter model={model} />
+        <MODEL.Provider value={model.reload}>
+          <PropertyFilter />
+        </MODEL.Provider>
       </RSplit>
     </>
   );