"Uncaught TypeError: Cannot read property 'isDestroyed' of undefined"

[poizan42]

1. Write anything that fails checking, no matter how trivial. Checking a file that just contains the word "blah" is enough.
2. Place cursor at end of file
3. Press Ctrl+Shift+I

Atom Version: 1.3.2
System: Microsoft Windows 10 Pro Insider Preview
Thrown From: fstar-interactive package, v0.1.0

Stack Trace

Uncaught TypeError: Cannot read property 'isDestroyed' of undefined

At C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:304

TypeError: Cannot read property 'isDestroyed' of undefined
    at C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:304:15
    at C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:206:64

Commands

  4x -7:28.6.0 core:backspace (atom-text-editor.editor.is-focused)
     -7:24.4.0 core:move-left (atom-text-editor.editor.is-focused)
     -6:53.9.0 core:save (atom-text-editor.editor.is-focused)
     -6:23.8.0 fstar-interactive:trigger (atom-text-editor.editor.is-focused)
     -6:12 core:save (atom-notification.fatal.icon.icon-bug.native-key-bindings.has-detail.has-close.has-stack)
  2x -6:09.2.0 fstar-interactive:trigger (atom-text-editor.editor.is-focused)
     -0:12.3.0 core:move-down (atom-text-editor.editor.is-focused)
     -0:02.6.0 fstar-interactive:trigger (atom-text-editor.editor.is-focused)

Config

{}

Installed Packages

# User
fstar-interactive, v0.1.0
language-fstar, v0.1.0

# Dev
No dev packages

[poizan42]

I don't really have any idea about the api of Atom, but I couldn't help but notices that the code in the clearAllMarkers function actually checks for truthiness of the marker:

this.markers.forEach(function(marker) { if(marker && !marker.isDestroyed()) { marker.destroy(); } } );

But the popMarker function where this error occurs does not:

...
        var m = _this.markers.shift();
        _this.child.stdin.write("#pop\n");
        if (!m.isDestroyed()) { // <-- error here
          m.already_popped = true;
          m.destroy();
        }
...

[poizan42]

So I tried stepping through the code, and the reason m is undefined is because the array is empty and we never found the marker that we were looking for.

Console output:

Build command: --in
 cwd = C:\Users\poizan\Documents\fstar
C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:240Calling process with args: <--in>
C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:411Not an error line : <#fail
>
C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:411Not an error line : <>
C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:417ERROR!:
<input>(1,5-1,5): Syntax error: Parsing.Parse_error,<input>,1,5,1,5, Syntax error: Parsing.Parse_error
C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:460Marking region: (0, 5),(0, 6)
 marker range is [(0, 4) - (0, 4)]
C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:461Text of region is []
C:\Users\poizan\Documents\dev\fstar-interactive\lib\main.js:210<input>(1,5-1,5): Syntax error: Parsing.Parse_error
#fail

The value of the arguments:

marker
TextEditorMarker {layer: TextEditorMarkerLayer, bufferMarker: Marker, displayBuffer: DisplayBuffer, emitter: Emitter, disposables: CompositeDisposable…}
bufferMarker: Marker
displayBuffer: DisplayBuffer
disposables: CompositeDisposable
emitter: Emitter
id: "0-371"
layer: TextEditorMarkerLayer
__proto__: TextEditorMarker

ev
Object {check_failed: true}

And the markers:

_this.markers.length
2

_this.markers[0]
TextEditorMarker {layer: TextEditorMarkerLayer, bufferMarker: Marker, displayBuffer: DisplayBuffer, emitter: Emitter, disposables: CompositeDisposable…}
bufferMarker: Marker
displayBuffer: DisplayBuffer
disposables: CompositeDisposable
emitter: Emitter
hasChangeObservers: true
id: "0-371"
layer: TextEditorMarkerLayer
oldHeadBufferPosition: Point
oldHeadScreenPosition: Point
oldTailBufferPosition: Point
oldTailScreenPosition: Point
wasValid: true
__proto__: TextEditorMarker

_this.markers[1]
TextEditorMarker {layer: TextEditorMarkerLayer, bufferMarker: Marker, displayBuffer: DisplayBuffer, emitter: Emitter, disposables: CompositeDisposable…}
bufferMarker: Marker
displayBuffer: DisplayBuffer
disposables: CompositeDisposable
emitter: Emitter
id: "0-370"
layer: TextEditorMarkerLayer
__proto__: TextEditorMarker

Note that _this.markers[0].id === marker.id but

_this.markers[0] === marker
false

Same id, but different objects

[poizan42]

Replacing

if (m === marker)

With

if (m.id === marker.id)

seems to fix this. I have no idea if that is the proper way to do it though.