Recent Changes - Search:




A step console is just like a shell, except that you are not expected to write commands directly in the prompt. Instead you have a different input window from where the commands are issued, and in practice you'll have in this window whole list of commands that you intend to send to the process one by one and enjoy the feedback. In contrast to the notion of Pipes.Worksheets, the output is not directed back to the window where the commands are issued; they are displayed in the shell window.

So you can regard it as an automatisation of doing copy-and-paste from a programme listing to the shell. The main feature is a mechanism to detect which is the next command in the programme listing, either in terms of syntax or in terms of layout, and send it to the shell. One use of this is to debug programmes: go through it step by step, just hitting <enter> all the time, and at each step see the result.

Clearly, a step console needs a working shell-like window, and there seems to be no reason for disallowing input also in the console, if the user suddenly prefers, so we will henceforth assume the console is a fully functional shell, and hence a step-console is just an extra interface to a shell.

Step consoles make sense for all situation where a shell makes sense, and eventually every Alpha mode which is also associated to some external interpreter could have step functionality. (Tcl mode has some evaluate functionality for evaluating regions, but it doesn't step!)

But there are situations where this sort of interface is particularly appropriate: namely in situation where the feedback from the external process are not really return values, but rather some sort of messages or reports. You wouldn't want to have these messages written back into your programme file like in a worksheet, or engrave them anywhere at all --- they are merely helpful messages as you step through the programme --- and the pure shell interface comes short for the same reason: you don't want the actual commands you are issuing to get lost in the confusion of real time messages on the screen. It is better to keep them separate in a different window for reediting and later use.

'''Example: interaction with 'Coq' '''

See Modes.CoqMode.

One example where the feedback from the programme consists rather in messages than proper return values, is 'coqtop', the top level command interpreter for 'coq'. Coq is is a proof assistant for automatising verification of mathematical proofs. The home page is . Proofs are written in the special-purpose lambda-calculus-like language 'gallina'. In the interactive mode (coqtop) you step through a proof and for each step coqtop reports if the step was properly justified or if it didn't understand a deduction, and displays messages about the state of the whole proof, subgoals and subtrees... Once the proof has been certified and the Qed statement succesfully issued, you won't bother anymore about those messages...

When Coq does not accept a step in your proof and gives an error message, you just edit the input to correct the shortcoming; then send it for evaluation again. In the end, when the proof has been corrected and blue-stamped, what is left in the input-sheet of the interface is the correct proof listings, not a transcript of an interactive session with all its messages and errors. In other words, it is a file you can later pass to coq in compile mode.


The only challenge in writing a step-console is properly to detect the input regions. This task will vary greatly from programme to programme. On the other hand, this problematic is found throughout Alpha, be it in isInComment procs, getContainer, nextFunction, embrace... Some problems concerning detecting regions for evaluation are also considered in the context of Pipes.Worksheets.

In coq, the main pattern used to determine the regions is the full-stop which marks the end of a statement. Hence roughly the region-determination proc looks backward for a full-stop and and then forward for the next full-stop and then selects the region in between.

Here comes the code listings for a primitive step-console interface to 'Coq'. Only the step-mechanism specific code is listed. So it is assumed that there is already a working shell-like interface to coqtop (like the ones outlines on the page Pipes.PipesAndShellLikeInteraction). (Note that coqtop sends the prompt via stderr, so the tricks explained at [Error pipes and window pipes] are necessary.)

The complete code for Modes.CoqMode can be downloaded from .

    ######## Set up the step functionality ########

    proc coq::send { } {
	variable coqMain
	if { [win::Current] == "*Coq console*" } {
	    variable promptPos
	    set cmd [getText $promptPos [getPos]]
	} else {
	    if { [isSelection] } {
		set cmd [getSelect]
		set next [selEnd]
	    } else {
		aimAt p0 p1
		set old $p0
		set cmd [getText $p0 $p1]
		set next $p1
	    if { [catch { nextRegion $next }] } {
		insertText {\r}
	if { [info exists cmd] } {
	    set cmd [stripComments $cmd]
	    set cmd [string trim $cmd]
	    insertText -w "*Coq console*" "$cmd\r"
	    puts $coqMain $cmd    

    proc coq::aimAt { pos0 pos1 } {
	upvar 1 $pos0 p0
	upvar 1 $pos1 p1
	if { [isSelection] } {
	    set p0 [getPos]
	    set p1 [selEnd]
	set pos [getPos]
	set backSearchPos [pos::math $pos - 2]
	if { [catch { search -f 0 -r 1 {\.\s+[^\s]} $backSearchPos } previous] } {
	    set p0 [minPos]
	} else {	
	    set p0 [pos::math [lindex $previous 1] -1]
	set forthSearchPos [pos::math $pos - 1]

	if { [catch { search -f 1 -r 1 {\.\r?} $forthSearchPos } next] } {
	    set p1 [maxPos]
	} else {
	    set p1 [lindex $next 1]

    # Select the next input region.  If no next input 
    # region is found an error is raised.
    proc coq::nextRegion { pos } {
	goto [pos::math $pos + 1]
	aimAt p0 p1
	select $p0 $p1

    proc coq::enter {} {
	if { ![isRunning] } {
	    variable win [win::Current]

	    after 500 {
		bringToFront $coq::win
		unset coq::win

	} else {
    ascii 0x03 coq::enter "coq"

    proc coq::isRunning {} {
	# A better check should be performed...
	if { [lsearch [winNames] "*Coq console*"] != -1 } {
	    return 1
	} else {
	    return 0

    proc coq::stripComments { txt } {
	set noOpeningOrClosing {(?:[^\(\*]|[\(][^\*]|[\*][^\)])*}
	# This means: we don't accept ( or *
	# except ( followed by anything else than *
	# and except * followed by anything else than )
	append commentExpr {\(*} ${noOpeningOrClosing} {\*+\)}
	# Note the plus: it is necessary to match a comment ending with **)
	set i 0
	while { [regsub -- $commentExpr $txt "" txt] } {
	    incr i
	return $txt
Page last modified on January 23, 2006, at 03:16 PM
Hosted on Logo