Re: [isabelle] isar-keywords

This is the ML code for the syntax,

val thms_parser = Scan.finite OuterLex.stopper (OuterParse.enum1 "," val add_rws_parser = OuterParse.reserved "add" -- OuterParse.$$$ ":" |-- thms_parser val del_rws_parser = OuterParse.reserved "del" -- OuterParse.$$$ ":" |-- thms_parser

val _ =
    OuterSyntax.command "modify_trs"
      "adds or deletes equations to the global term rewrite system"
      ((Scan.optional add_rws_parser [])
-- (Scan.optional del_rws_parser []) >> (fn (adds,dels) => Toplevel.theory (modify_TRS_cmd adds dels)))


On 31 Mar 2010, at 09:32, Makarius wrote:

On Tue, 30 Mar 2010, Omar Montano Rivas wrote:

*** 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?

To me this looks more like a problem in the outer syntax parser for your newly defined command. Can I see your ML definition for the syntax?


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.