pretty-printers pour le debugger

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

4 files changed, 38 insertions, 44 deletions

diff --git a/dev/base_db b/dev/base_db
new file mode 100644
index 000000000..c068b875c
--- /dev/null
+++ b/dev/base_db
@@ -0,0 +1,3 @@
+load_printer "top_printers.cmo"
+install_printer Top_printers.prid
+install_printer Top_printers.prsp
diff --git a/dev/base_include b/dev/base_include
index 8964873eb..f314b3558 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -47,14 +47,17 @@ let raw_constr_of_string s =
     (parse_ast s);;
 
 let e s    = 
-   constr_of_com Evd.empty (Global.env()) (parse_ast s);;
+   Astterm.constr_of_com Evd.empty (Global.env()) (parse_ast s);;
 
 (* Get the current goal *)
 
-let getgoal x = top_goal_of_pftreestate (get_pftreestate x);;
+let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);;
 
-let get_nth_goal n = nth_goal_of_pftreestate n (get_pftreestate ());;
+let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());;
 let current_goal () = get_nth_goal 1;;
 
 let pf_e gl s = 
-    constr_of_com (project gl) (pf_env gl) (parse_ast s);;
+    Astterm.constr_of_com (project gl) (pf_env gl) (parse_ast s);;
+
+open Toplevel
+let go = loop
diff --git a/dev/db b/dev/db
index 84223c745..2cb7bb5f3 100644
--- a/dev/db
+++ b/dev/db
@@ -1,4 +1,26 @@
-load_printer "db_printers.cmo"
-install_printer Db_printers.prid
-install_printer Db_printers.prsp
+load_printer "top_printers.cmo"
+install_printer Top_printers.prid
+install_printer Top_printers.prsp
+install_printer Top_printers.prast
+install_printer Top_printers.prastpat
+install_printer Top_printers.prastpatl
+
+install_printer Top_printers.pppattern
+install_printer Top_printers.pprawterm
+
+install_printer Top_printers.ppterm0
+install_printer Top_printers.print_uni
+install_printer Top_printers.pp_universes
+install_printer Top_printers.pptype
+install_printer Top_printers.prj
+
+install_printer Top_printers.prgoal
+install_printer Top_printers.prsigmagoal
+install_printer Top_printers.prctxt
+install_printer Top_printers.pproof
+install_printer Top_printers.prevd
+install_printer Top_printers.prevc
+install_printer Top_printers.prwc
+install_printer Top_printers.prclenv
+
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4b1a115af..cfe4d1b45 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -3,50 +3,16 @@
 
 open System
 open Pp
-open Coqast
 open Ast
-open Lexer
-open Egrammar
 open Names
 open Sign
 open Univ
-open Generic
-open Term
-open Sosub
 open Proof_trees
-open Summary
-open Libobject
-open Library
 open Environ
-open Termast
 open Printer
-open Closure
-open Reduction
-open Typing
-open Astterm
-open States
-open Constant
-open Inductive
-open Discharge
-open Command
-open Pretty
 open Refiner
 open Tacmach
-open Pfedit
 open Clenv
-open Tactics
-open Tacticals
-open Elim
-open Tacinterp
-open Tacentries
-open Vernacinterp
-open Vernacentries
-open Vernac
-open Toplevel
-open Mltop
-open Esyntax
-open Metasyntax
-
 
 let pP s = pP (hOV 0 s)
 
@@ -55,11 +21,11 @@ let prast c = pP(print_ast c)
 let prastpat c = pP(print_astpat c)
 let prastpatl c = pP(print_astlpat c)
 let ppterm0 = (fun x -> pP(term0 (gLOB nil_sign) x))
-let pprawterm = (fun x -> pP(prrawterm x));;
-let pppattern = (fun x -> pP(prpattern x));;
+let pprawterm = (fun x -> pP(prrawterm x))
+let pppattern = (fun x -> pP(prpattern x))
 let pptype = (fun x -> pP(prtype x))
 
-let prid id = pP [< 'sTR"#" ; 'sTR(string_of_id id) >]
+let prid id = pP [< 'sTR(string_of_id id) >]
 
 let prconst (sp,j) =
     pP [< 'sTR"#"; 'sTR(string_of_path sp);