From d2fd26a0ac600d066e79df4ab33b9bc924de069d Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 6 Oct 2012 10:08:40 +0000
Subject: remove dumptree.ml4

 This file was providing the "Dump Tree" command to display
 the state of a proof in XML. This command has been broken since
 the integration of Arnaud's proof engine. Nobody cared enough
 to adapt this to the new framework, moreover the trend is
 rather now to use the xml-base dialog mode of coqtop,
 so I simply remove this obsolete code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15870 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/xml/dumptree.ml4     | 109 -------------------------------------------
 plugins/xml/xml_plugin.mllib |   1 -
 2 files changed, 110 deletions(-)
 delete mode 100644 plugins/xml/dumptree.ml4

(limited to 'plugins/xml')

diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
deleted file mode 100644
index 1fd829e7a..000000000
--- a/plugins/xml/dumptree.ml4
+++ /dev/null
@@ -1,109 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This module provides the "Dump Tree" command that allows dumping the
-    current state of the proof stree in XML format *)
-
-(** Contributed by Cezary Kaliszyk, Radboud University Nijmegen *)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-open Tacexpr;;
-open Printer;;
-open Pp;;
-open Environ;;
-open Proof_type;;
-open Termops;;
-open Ppconstr;;
-open Names;;
-
-exception Different
-
-let xmlstream s = xmlescape s
-;;
-
-let thin_sign osign sign =
-  Sign.fold_named_context
-    (fun (id,c,ty as d) sign ->
-       try
-        if Sign.lookup_named id osign = (id,c,ty) then sign
-         else raise Different
-       with Not_found | Different -> Environ.push_named_context_val d sign)
-    sign ~init:Environ.empty_named_context_val
-;;
-
-let pr_var_decl_xml env (id,c,typ) =
-  let ptyp = print_constr_env env typ in
-  match c with
-  | None ->
-      (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\"/>")
-  | Some c ->
-      (* Force evaluation *)
-      let pb = print_constr_env env c in
-      (str "<hyp id=\"" ++ xmlstream (pr_id id) ++ str "\" type=\"" ++ xmlstream ptyp ++ str "\" body=\"" ++
-         xmlstream pb ++ str "\"/>")
-;;
-
-let pr_rel_decl_xml env (na,c,typ) =
-  let pbody = match c with
-    | None -> mt ()
-    | Some c ->
-	(* Force evaluation *)
-	let pb = print_constr_env env c in
-	  (str" body=\"" ++ xmlstream pb ++ str "\"") in
-  let ptyp = print_constr_env env typ in
-  let pid =
-    match na with
-    | Anonymous -> mt ()
-    | Name id -> str " id=\"" ++ pr_id id ++ str "\""
-  in
-  (str "<hyp" ++ pid ++ str " type=\"" ++ xmlstream ptyp ++ str "\"" ++ pbody ++ str "/>")
-;;
-
-let pr_context_xml env =
-  let sign_env =
-    fold_named_context
-      (fun env d pp -> pp ++ pr_var_decl_xml env d)
-      env ~init:(mt ())
-  in
-  let db_env =
-    fold_rel_context
-      (fun env d pp -> pp ++ pr_rel_decl_xml env d)
-      env ~init:(mt ())
-  in
-  (sign_env ++ db_env)
-;;
-
-let pr_subgoal_metas_xml metas env=
-  let pr_one (meta, typ) =
-    fnl () ++ str "<meta index=\"" ++ int meta ++ str " type=\"" ++ xmlstream (pr_goal_concl_style_env env typ) ++
-      str "\"/>"
-  in
-  List.fold_left (++) (mt ()) (List.map pr_one metas)
-;;
-
-let pr_goal_xml sigma g =
-  let env = try Goal.V82.unfiltered_env sigma g with _ -> empty_env in
-  if Decl_mode.try_get_info sigma g = None then
-    (hov 2 (str "<goal>" ++ fnl () ++ str "<concl type=\"" ++
-    xmlstream (pr_goal_concl_style_env env (Goal.V82.concl sigma g)) ++
-    str "\"/>" ++
-    (pr_context_xml env)) ++
-    fnl () ++ str "</goal>")
-  else
-    (hov 2 (str "<goal type=\"declarative\">" ++
-    (pr_context_xml env)) ++
-    fnl () ++ str "</goal>")
-;;
-
-let print_proof_xml () =
-  Errors.anomaly "Dump Tree command not supported in this version."
-
-
-VERNAC COMMAND EXTEND DumpTree
-  [ "Dump" "Tree" ] -> [ print_proof_xml () ]
-END
diff --git a/plugins/xml/xml_plugin.mllib b/plugins/xml/xml_plugin.mllib
index 655ea957e..27b0ef36f 100644
--- a/plugins/xml/xml_plugin.mllib
+++ b/plugins/xml/xml_plugin.mllib
@@ -7,5 +7,4 @@ Acic2Xml
 Xmlcommand
 Xmlentries
 Cic2Xml
-Dumptree
 Xml_plugin_mod
-- 
cgit v1.2.3