|
@@ -935,8 +935,8 @@ try
|
|
(* If we didn't find a completion point, load the display file in macro mode. *)
|
|
(* If we didn't find a completion point, load the display file in macro mode. *)
|
|
ignore(load_display_module_in_macro true);
|
|
ignore(load_display_module_in_macro true);
|
|
match ctx.com.display.dms_kind with
|
|
match ctx.com.display.dms_kind with
|
|
- | DMDefault ->
|
|
|
|
- | DMSignature -> raise (DisplayException(DisplaySignatures None))
|
|
|
|
|
|
+ | DMDefault -> raise (DisplayException(DisplayFields None))
|
|
|
|
+ | DMSignature -> raise (DisplayException(DisplaySignatures None))
|
|
| DMHover -> raise (DisplayException(DisplayHover None))
|
|
| DMHover -> raise (DisplayException(DisplayHover None))
|
|
| DMDefinition | DMTypeDefinition -> raise_positions []
|
|
| DMDefinition | DMTypeDefinition -> raise_positions []
|
|
| _ -> failwith "No completion point was found";
|
|
| _ -> failwith "No completion point was found";
|
|
@@ -1039,7 +1039,7 @@ with
|
|
| DisplayException(DisplayPackage pack) ->
|
|
| DisplayException(DisplayPackage pack) ->
|
|
DisplayPosition.display_position#reset;
|
|
DisplayPosition.display_position#reset;
|
|
raise (DisplayOutput.Completion (String.concat "." pack))
|
|
raise (DisplayOutput.Completion (String.concat "." pack))
|
|
- | DisplayException(DisplayFields(fields,cr,_)) ->
|
|
|
|
|
|
+ | DisplayException(DisplayFields Some(fields,cr,_)) ->
|
|
DisplayPosition.display_position#reset;
|
|
DisplayPosition.display_position#reset;
|
|
let fields = if !measure_times then begin
|
|
let fields = if !measure_times then begin
|
|
Timer.close_times();
|
|
Timer.close_times();
|