[plt-scheme] on-execute method in drscheme:language:language<%>

On Jun 16, Matthias Felleisen wrote:
> I think that's precisely what you don't want.

??

> This is an environmental issue not a programming issue. Suppose you
> are creating an executable.  All you want for this thing is to run;
> you don't want it to prove theorems, interactively, after you have
> carefully proven this program correct.

Sounds like it precisely what I *do* want!  To create an executable I
have to compile the file in advance -- the compilation process expands
macros, which forces me to prove the code correct.  The existence of
the compiled code becomes the certificate that the relevant proofs
were done.  Just like type-checking.


> On Jun 16, 2006, at 11:49 AM, Eli Barzilay wrote:
> 
> > On Jun 16, Dale Vaillancourt wrote:
> >> I need to "type-check" a program before running.  If it doesn't
> >> pass, I want to reject the attempt to run.  The checking is done by
> >> submitting the text in the definitions window to an external theorem
> >> prover.
> >>
> >> You are right about execute-callback not being quite what I want,
> >> btw.  That captures all clicks on `Run', even when my language is
> >> not the one associated with the current tab.
> >
> > Wouldn't that be better to do at syntax-expansion time?  Something
> > like overriding #%module-begin for module code, and the evaluation
> > handler for other toplevel interactions?  (And that will make it
> > possible to use outside of DrScheme.)
> >
> > -- 
> >           ((lambda (x) (x x)) (lambda (x) (x x)))          Eli 
> > Barzilay:
> >                   http://www.barzilay.org/                 Maze is 
> > Life!
> > _________________________________________________
> >   For list-related administrative tasks:
> >   http://list.cs.brown.edu/mailman/listinfo/plt-scheme
> 

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                  http://www.barzilay.org/                 Maze is Life!