30 …this.state = {};                                                                // Top and bottom …
31 …   this.state.current = {changed:false, bottom:null, top:null};                    // Current state  property
32 …this.state.future = null;                                                       // This state will…
33 …this.state.request = {top:null, bottom:null, upper:[], lower:[], full:false};   // Frozen state at…  property
41         if (!this.state.current.changed  &&  !this.firstPreview)
45         this.state.future = {changed:false, bottom:null, top:null};  property
55             this.state.request = { top:null, bottom:null, full:true};     property
62             this.state.request = this.getRequestState();            
75         var top = this.state.current.top;
81         var bottom = this.state.current.bottom;
85 …      const state = { top:top, bottom:bottom, upper:upperMatches, lower:lowerMatches, full:false };  variable
86         return state;
106         const top = this.state.request.top; 
107         const bottom = this.state.request.bottom; 
134         if (!this.state.future.changed) 
135             this.state.current = {changed:false, bottom:null, top:null};
148         var top = this.state.request.top;
151         var bottom = this.state.request.bottom;
154         this.updateDOM(top, bottom, html, this.state.request.full);
161         top = this.getExistingBoundaryMatch (headerMatches, this.state.request.upper);
162         bottom = this.getExistingBoundaryMatch (headerMatches, this.state.request.lower);
281         this.updateState(this.state.current, change);
282         this.updateState(this.state.future, change);
296         if (this.state.current.changed)
314     updateState (state, change) {  argument
317         if (state === null)
333         if (state.changed === false) {
334             state.top = top;
335             state.bottom = bottom;
336             state.changed = true;
339             if (state.top !== null)
340                 if (top === null  ||  top.endline < state.top.endline)
341                     state.top = top;
342             if (state.bottom !== null)
343                 if (bottom === null  ||  bottom.endline > state.bottom.endline)
344                     state.bottom = bottom;
352         const state = this.state.current;
355         if (!this.settings.highlight.dirty  ||  state.changed === false) {
362         const topline = state.top?.startline;
365         const bottomline = state.bottom?.endline;