[isabelle] isar-keywords



Hi,

I have a question regarding the use of keyword files in Isabelle2009-1. I have developed a theory A and obtained a keyword file ("isar-keyword-C.el") for my new command C using the method described in the isabelle's ML programming tutorial (http://isabelle.in.tum.de/nominal/activities/idp/ ). Now I want to build a new theory B on top of A using the command C. I have placed the file "isar-keyword-C.el" in "~/.isabelle/etc" and the command "isabelle emacs -k C" starts a new proof general session where the command C is being perfectly recognized. But when I try to build the theory B from the command line with "isabelle make" I get an error at the point where the new command C is used.

*** Stopper may not occur in input of finite scan!
*** At command "<malformed>" (line 29 of "...").

Is it possible to build B from the command line using "isabelle make" to get all the benefits of document preparation (latex, html, etc...)? Is the problem related with the isar-keyword file or it is something else?

Thanks,
Omar.


--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.