Uncaught TypeError: Cannot read property 'onDidChangeCursorPosition' of undefined

[catalin-hritcu]

TypeError: Cannot read property 'onDidChangeCursorPosition' of undefined
  at Object.module.exports.highlightErrors (/home/hritcu/Projects/fstar/fstar-interactive/lib/fstar-interactive.js:380:41)
  at Object.module.exports.onStdout (/home/hritcu/Projects/fstar/fstar-interactive/lib/fstar-interactive.js:168:14)
  at emitOne (events.js:77:13)
  at Socket.emit (events.js:166:7)
  at readableAddChunk (_stream_readable.js:146:16)
  at Socket.Readable.push (_stream_readable.js:109:10)
  at Pipe.onread (net.js:517:20)

The error was thrown from the fstar-interactive package.

[catalin-hritcu]

It happened when I was checking a large file and I switched to a different file before that was done.

[nikswamy]

Two points:

1. This seems related to @aseemr's addition of the click on the message bubble
2. Multiple file support isn't very good at the moment. If you switch files and start checking interactively the new one ... chaos will ensue. This should be fixed.

[aseemr]

I agree, with multiple files, all bets are off with the interactive mode. But I tried to reproduce the problem and could not. This is what I did:

1. Cmd-Shift-I on a large file, it triggers type checking (the file turns blue).
2. Shift to another file in a separate tab, press Cmd-Shift-I there, nothing happens.
3. Shift back to original file, it is still type checking, when type checking returns it's business as usual.

I also tried in step 2, instead of pressing Cmd-Shift-I, just stay on the tab for a long time (to ensure that type checking of the long file succeeds). Even then I did not get this exception.

Catalin: can you please try to reproduce this again ?

[nikswamy]

We could make it handle multiple files ... Spawning a separate background process for each interacting file.

[aseemr]

I was thinking the same, hopefully it would be a matter of restructuring code. I will try it.

[nikswamy]

What happens if you stay in step 2 above until the original file finishes type-checking. I suspect if we did that then the call to `atom.workspace.getActiveTextEditor' in the event handler waiting for the first call to finish will return the editor of the second file ... which may confuse things badly.

In any case, the current mode is written really with just a single file in mind. We should generalize it.

[aseemr]

The error highlighting did not work in that case, but I still did not get the exception ...

[catalin-hritcu]

@aseemr Yes, I can still reproduce this (when I'm not getting #6 at least). All I need to do is start type-checking tinyfstar-new.fst and then switch to a different file it seems. Screenshot attached:

[nikswamy]

Are you trying to feed f* more than one module in the interactive mode? That's not supported.

Sent from my Windows Phone

---

From: Catalin Hritcumailto:notifications@github.com Sent: ‎5/‎23/‎2015 23:24 To: FStarLang/fstar-interactivemailto:fstar-interactive@noreply.github.com Cc: nikswamymailto:nswamy@live.com Subject: Re: [fstar-interactive] Uncaught TypeError: Cannot read property 'onDidChangeCursorPosition' of undefined (#5)

@aseemr Yes, I can still reproduce this (when I'm not getting #6 at least). All I need to do is start type-checking tinyfstar-new.fst and then switch to a different file it seems. Screenshot attached:

---

Reply to this email directly or view it on GitHub: https://github.com/FStarLang/fstar-interactive/issues/5#issuecomment-104983926

[catalin-hritcu]

Yes. So is only #6 not a bug but a missing feature, or also this one?

[aseemr]

1. I see a different error this time. Cannot read markBuferRange of undefined, it's different from the original error.
2. What do you mean switch to a different file ? Do you just select a different file tab and keep it on screen until the type checking of tiny-fstar.fst finishes, or something else ? Can you please add some detailed steps ? I still cannot get it on my machine.

[catalin-hritcu]

1. I see a different error this time. Cannot read markBuferRange of undefined, it's different from the original error.

I've also got this one this time; see screenshot.

TypeError: Cannot read property 'markBufferRange' of undefined
  at /home/hritcu/Projects/fstar/fstar-interactive/lib/fstar-interactive.js:389:35
  at Array.forEach (native)
  at Object.module.exports.highlightErrors (/home/hritcu/Projects/fstar/fstar-interactive/lib/fstar-interactive.js:385:17)
  at Object.module.exports.onStdout (/home/hritcu/Projects/fstar/fstar-interactive/lib/fstar-interactive.js:168:14)
  at emitOne (events.js:77:13)
  at Socket.emit (events.js:166:7)
  at readableAddChunk (_stream_readable.js:146:16)
  at Socket.Readable.push (_stream_readable.js:109:10)
  at Pipe.onread (net.js:517:20)

2 What do you mean switch to a different file ? Do you just select a different file tab and keep it on screen until the type checking of tiny-fstar.fst finishes, or something else ?

Yes, exactly this. I just hit Ctrl + Shift + I at the end of tinyfstar-new.fst and then switch to the Settings tab.

Can you please add some detailed steps ? I still cannot get it on my machine.

It seems to help in reproducing this to switch to the Settings tab, as opposed to a file. Probably the Settings tab has a lot less of the properties that the plugin needs. Switching to a different file seems more likely to just silently fail.

[aseemr]

Thanks Catalin. I was able to reproduce it. Seems to be fixed now after my latest commit to support multiple files (https://github.com/FStarLang/fstar-interactive/commit/6f4d989c3614d5674959a451d5d08fbd2659e889).