kweb does not kompile a definition typed in the original window

[grosu]

I just tried to type a simple program in the original kweb window to demonstrate K, and it gave me an error saying that no file has been selected. We need something better there.

[pdaian]

Thanks for reporting the issue, I admit this was a use case I overlooked in the original design of kweb.

So there are several general solutions I can think of off the top of my head, let me know which one you prefer and we can further refine:

• Do not allow input in the "anonymous file" (default window file with no filename) by disabling/graying out the input box on the first page load. We can even put a default tutorial on using kweb in that box by default. The advantages here is that this is the simplest change and maintains the user workflow of the current kweb. Disadvantages being that the user must create a file if they want to run something not in the tutorial.
• Come up with a default name for the anonymous file, open it automatically. For example, 1_tutorial/hello_world. I'm not a big fan of this idea as it constrains the user by making it difficult for them to write K definitions, etc. when different file formats are required.
• If the user edits the default file, prompt them for a new filename and create a new file for them. The only issue with this is that the user also needs to specify a directory to put the file in, introducing some UI challenges.

If you have another idea for how this should work I'm of course always open. Let me know :).

[grosu]

From a user perspective, the simplest approach would be not worry about any name for that file. Just type in something and then click kompile. But this is risky, because one may lose the entire thing or have a headache searching if one switches to a program.

So your first solution is perhaps best. Just have some quick instructions in the original frame, telling people that they need to either create a new file (recommended into a unique folder) or modify an existing one.

Grigore

Sent from phone

-------- Original message -------- From: pdaian Date:03/08/2014 06:41 (GMT-06:00) To: kframework/kweb Cc: "Rosu, Grigore" Subject: Re: [kweb] kweb does not kompile a definition typed in the original window (#12)

Thanks for reporting the issue, I admit this was a use case I overlooked in the original design of kweb.

So there are several general solutions I can think of off the top of my head, let me know which one you prefer and we can further refine:

• Do not allow input in the "anonymous file" (default window file with no filename) by disabling/graying out the input box on the first page load. We can even put a default tutorial on using kweb in that box by default. The advantages here is that this is the simplest change and maintains the user workflow of the current kweb. Disadvantages being that the user must create a file if they want to run something not in the tutorial.
• Come up with a default name for the anonymous file, open it automatically. For example, 1_tutorial/hello_world. I'm not a big fan of this idea as it constrains the user by making it difficult for them to write K definitions, etc. when different file formats are required.
• If the user edits the default file, prompt them for a new filename and create a new file for them. The only issue with this is that the user also needs to specify a directory to put the file in, introducing some UI challenges.

If you have another idea for how this should work I'm of course always open. Let me know :).

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/kweb/issues/12#issuecomment-37096628.

[pdaian]

Sounds good, I like that solution a lot because it's simple to create and we can potentially put some rich HTML instructions in that textbox. Will update within 24 hours with a patch. Thanks again for reporting!

[pdaian]

@grosu this should be fixed now. Let me know if the solution is not OK.