No longer used (and probably no longer working) code removed.

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

1 files changed, 1 insertions, 272 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 63f7bfce2..ace8a7435 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -19,7 +19,7 @@
 
 (* CONFIGURATION PARAMETERS *)
 
-let verbose = ref false;; (* always set to true during a "Print XML All" *)
+let verbose = ref false;;
 
 (* HOOKS *)
 let print_proof_tree, set_print_proof_tree =
@@ -557,277 +557,6 @@ let show fn =
   show_pftreestate fn (kind,pftst) id
 ;;
 
-(*
-(* FUNCTIONS TO PRINT AN ENTIRE SECTION OF COQ *)
-
-(* list of (name, uncooked sp, most cooked sp, uncooked leaf object,  *)
-(*          list of possible variables, directory name)               *)
-(* used to collect informations on the uncooked and most cooked forms *)
-(* of objects that could be cooked (have namesakes)                   *)
-let printed = ref [];;
-
-(* makes a filename from a directory name, a section path and an extension *)
-let mkfilename dn sp ext =
-(*CSC:
- let dir_list_of_dirpath s =
-  let rec aux n =
-   try
-    let pos = String.index_from s n '/' in
-    let head = String.sub s n (pos - n) in
-     head::(aux (pos + 1))
-   with
-    Not_found -> [String.sub s n (String.length s - n)]
-  in
-   aux 0
- in
-  let module L = Library in
-  let module S = System in
-  let module N = Names in
-  let module No = Nameops in
-   match dn with
-      None         -> None
-    | Some basedir ->
-	let dir0 = No.extend_dirpath (No.dirpath sp) (No.basename sp) in
-	let dir = List.map N.string_of_id (List.rev (N.repr_dirpath dir0)) in
-       Some (join_dirs basedir dir ^ "." ^ ext)
-*) match dn with None -> None | Some _ -> Some "/tmp/nonloso"
-;;
-
-(* print_coq_object leaf_object id section_path directory_name formal_vars  *)
-(*  where leaf_object    is a leaf object                                   *)
-(*  and   id             is the identifier (name) of the definition/theorem *)
-(*                       or of the inductive definition o                   *)
-(*  and   section_path   is the section path of o                           *)
-(*  and   directory_name is the base directory in which putting the print   *)
-(*  and   formal_vars    is the list of parameters (variables) of o         *)
-(* pretty prints via Xml.pp the object o in the right directory deduced     *)
-(* from directory_name and section_path                                     *)
-(* Note: it is printed only the uncooked available form of the object plus  *)
-(*       the list of parameters of the object deduced from it's most cooked *)
-(*       form                                                               *)
-let print_coq_object lobj id sp dn fv env =
- let module D = Declarations in
- let module E = Environ in
- let module G = Global in
- let module N = Names in
- let module T = Term in
- let module X = Xml in
-(*CSC: GROSSO BUG: env e' l'environment cumulativo in cui aggiungiamo passo passo tutte le variabili. Qui, invece, non lo stiamo piu' usando per nulla. Quindi la prima variabile che incontreremo non verra' trovata ;-(((( Direi che l'environment vada passato fino alla print_object che a sua volta lo passera' a chi di dovere (ovvero sia a Cic2Acic che a DoubleTypeInference *)
-  let strtag = Libobject.object_tag lobj in
-   try
-    let tag = tag_of_string_tag strtag in
-    let obj =
-     match strtag with
-        "CONSTANT"  (* = Definition, Theorem, Axiom *)
-          let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} =
-           G.lookup_constant sp
-          in
-           mk_constant_obj id val0 typ fv hyps
-      | "INDUCTIVE" ->
-           let
-            {D.mind_packets=packs ;
-             D.mind_hyps = hyps;
-             D.mind_finite = finite
-            } = G.lookup_mind sp
-           in
-            mk_inductive_obj sp packs fv hyps finite
-      | "VARIABLE" ->
-          let (_,(_,varentry,_)) = Declare.out_variable lobj in
-           begin
-            match varentry with
-               Declare.SectionLocalDef (body,optt,opaq) ->
-                 let typ = match optt with
-		   | None -> Retyping.get_type_of env Evd.empty body 
-		   | Some t -> t in
-                 add_to_pvars (Definition (N.string_of_id id, body, typ)) ;
-                 mk_variable_obj id (Some body) typ
-             | Declare.SectionLocalAssum typ ->
-                add_to_pvars (Assumption (N.string_of_id id, typ)) ;
-                mk_variable_obj id None (T.body_of_type typ)
-           end
-      | "CLASS"
-      | "COERCION"
-      | _ -> raise Uninteresting
-    in
-     let fileext () = ext_of_tag tag in
-     let fn = mkfilename dn sp (fileext ()) in
-      print_object (uri_of_path sp tag) obj Evd.empty None fn
-   with
-    Uninteresting -> ()
-;;
-
-(* print_library_segment state bprintleaf directory_name                      *)
-(*  where state          is a list of (section-path, node)                    *)
-(*  and   bprintleaf     is true iff the leaf objects should be printed       *)
-(*  and   directory_name is the name of the base directory in which to print  *)
-(*                       the files                                            *)
-(* print via print_node all the nodes (leafs excluded if bprintleaf is false) *)(* in state                                                                   *)
-let rec print_library_segment state bprintleaf dn =
-  List.iter
-   (function (sp, node) ->
-     print_if_verbose ("Print_library_segment: " ^ Names.string_of_path sp ^ "\n") ;
-     print_node node (Nameops.basename sp) sp bprintleaf dn ;
-     print_if_verbose "\n"
-   ) (List.rev state)
-(* print_node node id section_path bprintleaf directory_name             *)
-(* prints a single node (and all it's subnodes via print_library_segment *)
-and print_node n id sp bprintleaf dn =
- let module L = Lib in
-  match n with
-     L.Leaf o ->
-      print_if_verbose "LEAF\n" ;
-      if bprintleaf then
-       begin
-         if not (List.mem id !printed) then
-          (* this is an uncooked term or a local (with no namesakes) term *)
-          begin
-(*CSC: pezza quando i .vo sono magri
-try
-*)
-           if could_have_namesakes o sp then
-            begin
-             (* this is an uncooked term *)
-             print_if_verbose ("OK, stampo solo questa volta " ^ Names.string_of_id id ^ "\n") ;
-             print_coq_object o id sp dn !pvars !cumenv ;
-             printed := id::!printed
-            end
-           else
-            begin
-             (* this is a local term *)
-             print_if_verbose ("OK, stampo " ^ Names.string_of_id id ^ "\n") ;
-             print_coq_object o id sp dn !pvars !cumenv
-            end
-(*CSC: pezza quando i .vo sono magri
-with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
-*)
-          end
-         else
-          begin
-           (* update the least cooked sp *)
-           print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n")
-          end
-       end
-   | L.OpenedSection (dir,_) ->
-       let id = snd (Nameops.split_dirpath dir) in
-       print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n")
-   | L.ClosedSection (_,dir,state) ->
-      let id = snd (Nameops.split_dirpath dir) in
-      print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ;
-      if bprintleaf then
-       begin
-        (* open a new scope *)
-        let (_,section_name) = Nameops.split_dirpath dir in
-         pvars := (section_name,[])::!pvars ;
-         print_library_segment state bprintleaf dn ;
-         (* close the scope *)
-         match !pvars with
-            [] -> assert false
-          | he::tl -> pvars := tl
-       end ;
-      print_if_verbose "/ClosedDir\n"
-   | L.Module s ->
-      print_if_verbose ("Module " ^ (Names.string_of_dirpath s) ^ "\n")
-   | L.FrozenState _ ->
-      print_if_verbose ("FrozenState\n")
-;;
-
-(* print_closed_section module_name node directory_name                      *)
-(*  where module_name is the name of a module                                *)
-(*  and   node is the library segment of the module                          *)
-(*  and   directory_name is the base directory in which to put the xml files *)
-(* prints all the leaf objects of the tree rooted in node using              *)
-(* print_library_segment on all its sons                                     *)
-let print_closed_section s ls dn =
- let module L = Lib in
-  printed := [] ;
-  pvars := [Names.id_of_string "",[]] ;
-  cumenv := Safe_typing.env_of_safe_env (Global.safe_env ()) ;
-  print_if_verbose ("Module " ^ s ^ ":\n") ;
-  print_library_segment ls true dn ;
-  print_if_verbose "\n/Module\n" ;
-;;
-
-(* printModule identifier directory_name                                     *)
-(*  where identifier     is the name of a module (section) d                 *)
-(*  and   directory_name is the directory in which to root all the xml files *)
-(* prints all the xml files and directories corresponding to the subsections *)
-(* 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 (loc,qid) dn =
- let module L = Library in
- let module N = Nametab in
- let module X = Xml in
-
-  let (_,dir_path,_) = L.locate_qualified_library qid in
-
-  let str = N.string_of_qualid qid in 
-  let ls = L.module_segment (Some dir_path) in
-   print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^
-    (L.module_full_filename dir_path) ^ "\n") ;
-   print_closed_section str (List.rev ls) dn ;
-   print_if_verbose ("MODULE_END " ^ str ^ " " ^
-    (L.module_full_filename dir_path) ^ "\n")
-;;
-
-(* printSection identifier directory_name                                    *)
-(*  where identifier     is the name of a closed section d                   *)
-(*  and   directory_name is the directory in which to root all the xml files *)
-(* prints all the xml files and directories corresponding to the subsections *)
-(* and terms of the closed section d                                         *)
-(* Note: the terms are printed in their uncooked form plus the informations  *)
-(* on the parameters of their most cooked form                               *)
-let printSection id dn =
- let module L = Library in
- let module N = Names in
- let module No = Nameops in
- let module X = Xml in
-  let sp = Lib.make_path id in
-  let ls =
-   let rec find_closed_section =
-    function
-       [] -> raise Not_found
-     | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (No.split_dirpath dir) = id
-	 -> ls
-     | _::t -> find_closed_section t
-   in
-    print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ;
-    find_closed_section (Lib.contents_after None)
-  in
-  let str = N.string_of_id id in 
-   print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ "\n");
-   print_closed_section str ls dn ;
-   print_if_verbose ("SECTION_END " ^ str ^ " " ^ N.string_of_path sp ^ "\n")
-;;
-
-(* print All () prints what is the structure of the current environment of *)
-(* Coq. No terms are printed. Useful only for debugging                    *)
-let printAll () =
- let state = Library.module_segment None in
-  let oldverbose = !verbose in
-   verbose := true ;
-   print_library_segment state false None ;
-(*
-   let ml = Library.loaded_modules () in
-    List.iter (function i -> printModule (Names.id_of_string i) None) ml ;
-*)
-    verbose := oldverbose
-;;
-*)
-
-
-(*CSC: Ask Hugo for a better solution *)
-(*
-let ref_of_kernel_name kn =
- let module N = Names in
- let module Ln = Libnames in
-  let (modpath,_,label) = N.repr_kn kn in
-   match modpath with
-      N.MPself _ -> Ln.Qualid (Ln.qualid_of_sp (Nametab.sp_of_global None kn))
-    | _ ->
-      Util.anomaly ("ref_of_kernel_name: the module path is not MPself")
-;;
-*)
 
 (* Let's register the callbacks *)
 let xml_library_root =