diff options
Diffstat (limited to 'contrib/xml/xmlentries.ml4')
-rw-r--r-- | contrib/xml/xmlentries.ml4 | 131 |
1 files changed, 131 insertions, 0 deletions
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4 new file mode 100644 index 000000000..d81269702 --- /dev/null +++ b/contrib/xml/xmlentries.ml4 @@ -0,0 +1,131 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* A module to print Coq objects in XML *) +(* *) +(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) +(* 06/12/2000 *) +(* *) +(* This module adds to the vernacular interpreter the functions that fullfill *) +(* the new commands defined in Xml.v *) +(* *) +(******************************************************************************) +(*i camlp4deps: "parsing/grammar.cma" i*) + +(* $Id$ *) + +open Util;; +open Vernacinterp;; + +open Extend;; +open Genarg;; +open Pp;; +open Pcoq;; + +(* File name *) + +let wit_filename, rawwit_filename = Genarg.create_arg "filename" +let filename = Pcoq.create_generic_entry "filename" rawwit_filename +let _ = Tacinterp.add_genarg_interp "filename" + (fun ist x -> + (in_gen wit_filename + (out_gen (wit_opt wit_string) + (Tacinterp.genarg_interp ist + (in_gen (wit_opt rawwit_string) + (out_gen rawwit_filename x)))))) + +GEXTEND Gram + GLOBAL: filename; + filename: [ [ IDENT "File"; fn = STRING -> Some fn | -> None ] ]; +END + +let pr_filename = function Some fn -> str " File" ++ str fn | None -> mt () + +let _ = + Pptactic.declare_extra_genarg_pprule + (rawwit_filename, pr_filename) + (wit_filename, pr_filename) + +(* Disk name *) + +let wit_diskname, rawwit_diskname = Genarg.create_arg "diskname" +let diskname = create_generic_entry "diskname" rawwit_diskname +let _ = Tacinterp.add_genarg_interp "diskname" + (fun ist x -> + (in_gen wit_diskname + (out_gen (wit_opt wit_string) + (Tacinterp.genarg_interp ist + (in_gen (wit_opt rawwit_string) + (out_gen rawwit_diskname x)))))) + +GEXTEND Gram + GLOBAL: diskname; + diskname: [ [ IDENT "Disk"; fn = STRING -> Some fn | -> None ] ]; +END + +open Pp + +let pr_diskname = function Some fn -> str " Disk" ++ str fn | None -> mt () + +let _ = + Pptactic.declare_extra_genarg_pprule + (rawwit_diskname, pr_diskname) + (wit_diskname, pr_diskname) + +VERNAC COMMAND EXTEND Xml +| [ "Print" "XML" filename(fn) qualid(id) ] -> [ Xmlcommand.print id fn ] + +| [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ] + +| [ "Print" "XML" "All" ] -> [ Xmlcommand.printAll () ] + +| [ "Print" "XML" "Module" diskname(dn) qualid(id) ] -> + [ Xmlcommand.printModule id dn ] + +| [ "Print" "XML" "Section" diskname(dn) ident(id) ] -> + [ Xmlcommand.printSection id dn ] +END +(* +vinterp_add "Print" + (function + [VARG_QUALID id] -> + (fun () -> Xmlcommand.print id None) + | [VARG_QUALID id ; VARG_STRING fn] -> + (fun () -> Xmlcommand.print id (Some fn)) + | _ -> anomaly "This should be trapped");; + +vinterp_add "Show" + (function + [] -> + (fun () -> Xmlcommand.show None) + | [VARG_STRING fn] -> + (fun () -> Xmlcommand.show (Some fn)) + | _ -> anomaly "This should be trapped");; + +vinterp_add "XmlPrintAll" + (function + [] -> (fun () -> Xmlcommand.printAll ()) + | _ -> anomaly "This should be trapped");; + +vinterp_add "XmlPrintModule" + (function + [VARG_QUALID id] -> (fun () -> Xmlcommand.printModule id None) + | [VARG_QUALID id ; VARG_STRING dn] -> + (fun () -> Xmlcommand.printModule id (Some dn)) + | _ -> anomaly "This should be trapped");; + +vinterp_add "XmlPrintSection" + (function + [VARG_IDENTIFIER id] -> (fun () -> Xmlcommand.printSection id None) + | [VARG_IDENTIFIER id ; VARG_STRING dn] -> + (fun () -> Xmlcommand.printSection id (Some dn)) + | _ -> anomaly "This should be trapped");; +*) |