[plt-dev] #lang: the stake in Dracula's heart?

Can't the language come with code that makes the

  #lang acl2

line appear and disappear on write/read from the program's file?

As for sending it from drscheme to the ACL2 theorem prover, I
imagine that this is all under your control. -- Matthias







On Feb 1, 2010, at 2:16 PM, Carl Eastlund wrote:

> On Mon, Feb 1, 2010 at 2:05 PM, Robby Findler
> <robby at eecs.northwestern.edu> wrote:
>> On Mon, Feb 1, 2010 at 1:03 PM, Carl Eastlund <cce at ccs.neu.edu>  
>> wrote:
>>> On Mon, Feb 1, 2010 at 1:02 PM, Matthew Flatt <mflatt at cs.utah.edu>  
>>> wrote:
>>>> If a file extension is the only way to declare ACL2, then you'd  
>>>> have to
>>>> save a file in DrScheme to use the ACL2 language.
>>>
>>> I am fairly certain that other editors can save files with a ".lisp"
>>> extension, so I don't know what you mean here.
>>
>> He means that unsaved files won't know what language they are  
>> supposed
>> to be in, I expect.
>
> Oh, unsaved files.  I see.  What about just opening the Language menu
> and selecting ACL2?
>
> --Carl
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-dev