Email Gateway (Aug 18 2022 at 14:50): Email Gateway (Aug 18 2022 at 14:50):From: Omar Montano Rivas <O.Montano-Rivas-2@sms.ed.ac.uk>
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.
Email Gateway (Aug 18 2022 at 14:50):From: Makarius <makarius@sketis.net>
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?
Makarius
Email Gateway (Aug 18 2022 at 14:50):From: Makarius <makarius@sketis.net>
The thms_parser with its own invocation of Scan.finite looks very odd --
it is probably imported from some of Christian Urban's examples on playing
with the scanner framework independently from Isar outer syntax. If you
just use (OuterParse.enum1 "," OuterParse.name) instead it should work.
Anyway, the whole modify_trs command looks like just a plain add/del
declaration of theorems to the context. This can be done more
conveniently and more flexibly via an "attribute", not a command.
Isar attributes can be used in many places, e.g. as follows
declare blah [trs add]
or within a proof:
note blah [trs del]
or more -- the above are just typical examples.
In Isabelle2009-1/src/Pure/Tools/named_thms.ML we have something like a
canonical example of managing a plain list of theorems within the context,
together with add/del attribute definition. The latter can also be done
in Isar via the attribute_setup command. You can also use Named_Thms
directly as a simplistic solution, if there are no special demands for
indexing the content (although proper indexing is usually required for
advanced tools).
Makarius
Email Gateway (Aug 18 2022 at 14:50):From: Omar Montano Rivas <O.Montano-Rivas-2@sms.ed.ac.uk>
This is the ML code for the syntax,
val thms_parser = Scan.finite OuterLex.stopper (OuterParse.enum1 ","
OuterParse.name)
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"
OuterKeyword.thy_decl
((Scan.optional add_rws_parser [])
-- (Scan.optional del_rws_parser []) >> (fn (adds,dels) =>
Toplevel.theory (modify_TRS_cmd adds dels)))
Thanks,
Omar.
Last updated: Nov 21 2024 at 12:39 UTC