diff options
| author | herbelin | 2012-02-01 08:57:50 +0000 |
|---|---|---|
| committer | herbelin | 2012-02-01 08:57:50 +0000 |
| commit | 3be4b91c09e6ec816aada997fc245484abfa1f05 (patch) | |
| tree | 93bf666115190587026f183325b508f549d5d7ef | |
| parent | f7dba1c53fec7fe7ecefc4758e5a39c0010118b6 (diff) | |
Debugger vs tracer: Two different behaviors wrt printing: The debugger
runs in separate process. It has no access to the global env and it
should not request it. The tracer runs in the same process as Coq and
has full access to the global env and to regular pretty-printing of
global names.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14958 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | dev/base_include | 5 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 | ||||
| -rw-r--r-- | interp/constrextern.ml | 1 | ||||
| -rw-r--r-- | interp/constrextern.mli | 1 |
4 files changed, 10 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index d112596502..1c794a3ae9 100644 --- a/dev/base_include +++ b/dev/base_include @@ -199,6 +199,11 @@ let current_goal () = get_nth_goal 1;; let pf_e gl s = Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);; +(* Set usual printing since the global env is available from the tracer *) +let _ = Constrextern.in_debugger := false +let _ = Constrextern.set_debug_global_reference_printer + (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));; + open Toplevel let go = loop diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 3fc90761d1..3116cbf225 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -487,5 +487,9 @@ let short_string_of_ref loc = function [id_of_label (pi3 (repr_mind kn));id_of_string ("_"^string_of_int i)] (id_of_string ("_"^string_of_int j)) +(* Anticipate that printers can be used from ocamldebug and that + pretty-printer should not make calls to the global env since ocamldebug + runs in a different process and does not have the proper env at hand *) +let _ = Constrextern.in_debugger := true let _ = Constrextern.set_debug_global_reference_printer (if !rawdebug then raw_string_of_ref else short_string_of_ref) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bd8e78c0f5..b3810bb6d4 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -143,7 +143,6 @@ let debug_global_reference_printer = let in_debugger = ref false let set_debug_global_reference_printer f = - in_debugger := true; debug_global_reference_printer := f let extern_reference loc vars r = diff --git a/interp/constrextern.mli b/interp/constrextern.mli index e1fdd068b7..2a53eb85fe 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -53,6 +53,7 @@ val print_projections : bool ref (** Debug printing options *) val set_debug_global_reference_printer : (loc -> global_reference -> reference) -> unit +val in_debugger : bool ref (** This governs printing of implicit arguments. If [with_implicits] is on and not [with_arguments] then implicit args are printed prefixed |