Découpage des printers pour ne pas avoir de dépendances en la vm dans les printers de ocamldebug

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

1 files changed, 9 insertions, 98 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 5b9d2ac7c3..cef2ab9798 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -21,7 +21,6 @@ open Environ
 open Printer
 open Tactic_printer
 open Refiner
-open Tacmach
 open Term
 open Termops
 open Clenv
@@ -85,6 +84,15 @@ let prevd evd = pp(pr_evar_defs evd)
 let prclenv clenv = pp(pr_clenv clenv)
 let prgoal g = pp(db_pr_goal g)
 
+let pr_gls gls =
+  hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls))
+
+open Util
+
+let pr_glls glls =
+  hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++
+         prlist_with_sep pr_fnl db_pr_goal (sig_it glls))
+
 let prsigmagoal g = pp(pr_goal (sig_it g))
 let prgls gls = pp(pr_gls gls)
 let prglls glls = pp(pr_glls glls)
@@ -312,100 +320,3 @@ let _ =
 *)
 
 let ppfconstr c = ppterm (Closure.term_of_fconstr c)
-
-open Names
-open Cbytecodes
-open Cemitcodes
-open Vm
-
-let ppripos (ri,pos) =
-  (match ri with
-  | Reloc_annot a -> 
-      let sp,i = a.ci.ci_ind in
-      print_string 
-	("annot : MutInd("^(string_of_kn sp)^","^(string_of_int i)^")\n")
-  | Reloc_const _ ->
-      print_string "structured constant\n"
-  | Reloc_getglobal kn ->
-      print_string ("getglob "^(string_of_con kn)^"\n"));
-   print_flush ()
-
-let print_vfix () = print_string "vfix"
-let print_vfix_app () = print_string "vfix_app"
-let print_vswith () = print_string "switch"
-
-let ppsort = function
-  | Prop(Pos) -> print_string "Set"
-  | Prop(Null) -> print_string "Prop"
-  | Type u -> print_string "Type"
-
-
-
-let print_idkey idk =
-  match idk with 
-  | ConstKey sp -> 
-      print_string "Cons(";
-      print_string (string_of_con sp);
-      print_string ")"
-  | VarKey id -> print_string (string_of_id id)
-  | RelKey i -> print_string "~";print_int i
-
-let rec ppzipper z =
-  match z with 
-  | Zapp args -> 
-      let n = nargs args in
-      open_hbox ();
-      for i = 0 to n-2 do
-	ppvalues (arg args i);print_string ";";print_space()
-      done;
-      if n-1 >= 0 then ppvalues (arg args (n-1));
-      close_box()
-  | Zfix _ -> print_string "Zfix"
-  | Zswitch _ -> print_string "Zswitch"
-
-and ppstack s = 
-  open_hovbox 0;
-  print_string "[";
-  List.iter (fun z -> ppzipper z;print_string " | ") s;
-  print_string "]";
-  close_box()
-
-and ppatom a =
-  match a with
-  | Aid idk -> print_idkey idk
-  | Aiddef(idk,_) -> print_string "&";print_idkey idk
-  | Aind(sp,i) ->  print_string "Ind(";
-      print_string (string_of_kn sp);
-      print_string ","; print_int i;
-      print_string ")"
-  | Afix_app _ -> print_vfix_app ()
-  | Aswitch _ -> print_vswith()
-
-and ppwhd whd =
-  match whd with 
-  | Vsort s -> ppsort s
-  | Vprod _ -> print_string "product"
-  | Vfun _ -> print_string "function"
-  | Vfix _ -> print_vfix()
-  | Vfix_app _ -> print_vfix_app()
-  | Vcofix _ -> print_string "cofix"
-  | Vcofix_app _ -> print_string "cofix_app"
-  | Vconstr_const i -> print_string "C(";print_int i;print_string")"
-  | Vconstr_block b -> ppvblock b      
-  | Vatom_stk(a,s) ->
-      open_hbox();ppatom a;close_box();
-      print_string"@";ppstack s
-
-and ppvblock b =
-  open_hbox();
-  print_string "Cb(";print_int (btag b);
-  let n = bsize b in
-  for i = 0 to n -1 do
-    print_string ",";ppvalues (bfield b i)
-  done;
-  print_string")";
-  close_box()
-
-and ppvalues v =
-  open_hovbox 0;ppwhd (whd_val v);close_box();
-  print_flush()