diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 23 | ||||
| -rw-r--r-- | interp/constrextern.mli | 9 |
2 files changed, 18 insertions, 14 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 47753c1582..84baefe615 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -140,20 +140,21 @@ let insert_pat_alias loc p = function let extern_evar loc n l = if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None) -let debug_global_reference_printer = - ref (fun _ -> failwith "Cannot print a global reference") +(** We allow customization of the global_reference printer. + For instance, in the debugger the tables of global references + may be inaccurate *) -let in_debugger = ref false +let default_extern_reference loc vars r = + Qualid (loc,shortest_qualid_of_global vars r) -let set_debug_global_reference_printer f = - debug_global_reference_printer := f +let my_extern_reference = ref default_extern_reference -let extern_reference loc vars r = - if !in_debugger then - (* Debugger does not have the tables of global reference at hand *) - !debug_global_reference_printer loc r - else - Qualid (loc,shortest_qualid_of_global vars r) +let set_extern_reference f = my_extern_reference := f +let get_extern_reference () = !my_extern_reference + +let extern_reference loc vars l = !my_extern_reference loc vars l + +let in_debugger = ref false (**********************************************************************) (* mapping patterns to cases_pattern_expr *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 0e40e83e67..0a4192c3ea 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -51,9 +51,12 @@ val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref -(** Debug printing options *) -val set_debug_global_reference_printer : - (Loc.t -> global_reference -> reference) -> unit +(** Customization of the global_reference printer *) +val set_extern_reference : + (Loc.t -> Id.Set.t -> global_reference -> reference) -> unit +val get_extern_reference : + unit -> (Loc.t -> Id.Set.t -> global_reference -> reference) + val in_debugger : bool ref (** This governs printing of implicit arguments. If [with_implicits] is |