Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2720 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 138 insertions, 6 deletions

diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index b794b2893..3c06c00da 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -78,15 +78,16 @@ let extract_nparams pack =
 (* than that could exists in cooked form with the same name in a super        *)
 (* section of the actual section                                              *)
 let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
+ let module N = Nametab in
  let module D = Declare in
   let tag = Libobject.object_tag o in
    print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
    match tag with
       "CONSTANT" ->
         (match D.constant_strength sp with
-          | D.DischargeAt _  -> false (* a local definition *)
-          | D.NotDeclare     -> false (* not a definition *)
-          | D.NeverDischarge -> true  (* a non-local one    *)
+          | N.DischargeAt _  -> false (* a local definition *)
+          | N.NotDeclare     -> false (* not a definition *)
+          | N.NeverDischarge -> true  (* a non-local one    *)
         )
     | "PARAMETER"                 (* axioms and                               *)
     | "INDUCTIVE"       -> true   (* mutual inductive types are never local   *)
@@ -703,7 +704,7 @@ let pp_cmds_of_inner_types inner_types target_uri =
 (* Note: it is printed only (and directly) the most cooked available      *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-let print qid fn =
+let print (_,qid as locqid) fn =
  let module D = Declarations in
  let module G = Global in
  let module N = Names in
@@ -711,7 +712,7 @@ let print qid fn =
  let module T = Term in
  let module X = Xml in
   let (_,id) = Nt.repr_qualid qid in
-  let glob_ref = Nametab.locate qid in
+  let glob_ref = Nametab.global locqid in
   let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in
   reset_ids () ;
   let inner_types = ref [] in
@@ -976,7 +977,7 @@ let print_closed_section s ls dn =
 (* and terms of the module d                                                 *)
 (* Note: the terms are printed in their uncooked form plus the informations  *)
 (* on the parameters of their most cooked form                               *)
-let printModule qid dn =
+let printModule (loc,qid) dn =
  let module L = Library in
  let module N = Nametab in
  let module X = Xml in
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");;
+*)