diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index be60c9c307..bd8e78c0f5 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -140,14 +140,19 @@ let extern_evar loc n l = let debug_global_reference_printer = ref (fun _ -> failwith "Cannot print a global reference") +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 = - try Qualid (loc,shortest_qualid_of_global vars r) - with Not_found -> - (* happens in debugger *) + 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) + (************************************************************************) (* Equality up to location (useful for translator v8) *) @@ -371,7 +376,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = try - if !Flags.raw_print then raise Exit; + if !in_debugger || !Flags.raw_print then raise Exit; let projs = Recordops.lookup_projections (fst cstrsp) in let rec ip projs args acc = match projs with @@ -388,15 +393,17 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = CPatRecord(loc, List.rev (ip projs args [])) with Not_found | No_match | Exit -> + let c = extern_reference loc Idset.empty (ConstructRef cstrsp) in + if !in_debugger then CPatCstr (loc, c, args) else if !Topconstr.oldfashion_patterns then if pattern_printable_in_both_syntax cstrsp - then CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args) - else CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), add_patt_for_params cstrsp args) + then CPatCstr (loc, c, args) + else CPatCstrExpl (loc, c, add_patt_for_params cstrsp args) else let full_args = add_patt_for_params cstrsp args in match drop_implicits_in_patt cstrsp full_args with - |Some true_args -> CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), true_args) - |None -> CPatCstrExpl (loc, extern_reference loc vars (ConstructRef cstrsp), full_args) + |Some true_args -> CPatCstr (loc, c, true_args) + |None -> CPatCstrExpl (loc, c, full_args) in insert_pat_alias loc p na and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function |