|
@@ -1194,6 +1194,9 @@ try
|
|
|
| "usage" ->
|
|
|
activate_special_display_mode();
|
|
|
DMUsage
|
|
|
+ | "type" ->
|
|
|
+ activate_special_display_mode();
|
|
|
+ DMType
|
|
|
| "toplevel" ->
|
|
|
activate_special_display_mode();
|
|
|
DMToplevel
|
|
@@ -1460,7 +1463,7 @@ try
|
|
|
t();
|
|
|
if ctx.has_error then raise Abort;
|
|
|
begin match com.display with
|
|
|
- | DMNone | DMUsage | DMPosition | DMResolve _ ->
|
|
|
+ | DMNone | DMUsage | DMPosition | DMType | DMResolve _ ->
|
|
|
()
|
|
|
| _ ->
|
|
|
if ctx.has_next then raise Abort;
|