search

salmans / Razor

5 stars 0 forks source link

Displaying current depth #65

Open salmans opened 9 years ago

salmans commented 9 years ago

If the user enters @depth@ with no argument, we can display the current search depth instead of reporting a syntax error.

thedotmatrix commented 9 years ago

@salmans is the !c command for showing all configuration options not enough?

salmans commented 9 years ago

I agree that we have the functionality but because we have a separate function just to change the depth, I guess it's a good idea to be able to query depth independently. I am suggesting this as an enhancement; feel free to ignore it if you don't think it's a good idea or if it's not easy to implement.

thedotmatrix commented 9 years ago

I definitely agree with you. Specific feedback is definitely an enhancement that needs to happen. To me, this problem can be stated more generally for all the commands. As in, if depth is called with no argument, the repl will respond with what it expected, and any other relevant details. I will have to look into a nice systematic approach to this; the parsec library may have some interesting features that would help with this.

salmans commented 9 years ago

I think having a general/systematic solution for this kind of problems is a good idea. One thing that makes depth somehow more special is its awkward interaction with load: the fact that the user must set the right value for depth before loading the theory is not intuitive. I am trying to think of some way to make this parameter more accessible/bolder!

thedotmatrix commented 9 years ago

Revisiting this issue, I like the idea of load and depth becoming the same command, where the depth is an optional argument. It conveys that you're building something over the given theory to a particular depth.