more diagnostic operations;

--- a/src/Pure/Isar/proof_display.ML	Thu May 11 10:46:52 2023 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu May 11 12:20:47 2023 +0200
@@ -28,6 +28,9 @@
     ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Position.T -> Proof.context ->
     (string * typ -> bool) -> (string * typ) list -> unit
+  val markup_extern_label: Position.T -> (Markup.T * xstring) option
+  val print_label: Position.T -> string
+  val print_context_tracing: Context.generic * Position.T -> string
 end
 
 structure Proof_Display: PROOF_DISPLAY =
@@ -390,4 +393,30 @@
 
 end;
 
+
+(* position label *)
+
+val command_prefix = Markup.commandN ^ ".";
+
+fun markup_extern_label pos =
+  Position.label_of pos |> Option.map (fn label =>
+    (case try (unprefix command_prefix) label of
+      SOME cmd => (Markup.keyword1, Long_Name.base_name cmd)
+    | NONE => (Markup.empty, label)));
+
+fun print_label pos =
+  (case markup_extern_label pos of
+    NONE => ""
+  | SOME (m, s) => Markup.markup m s);
+
+
+(* context tracing *)
+
+fun context_type (Context.Theory _) = "theory"
+  | context_type (Context.Proof ctxt) =
+      if can Local_Theory.assert ctxt then "local_theory" else "Proof.context";
+
+fun print_context_tracing (context, pos) =
+  context_type context ^ (case print_label pos of "" => "" | s => " " ^ s) ^ Position.here pos;
+
 end;

--- a/src/Pure/PIDE/session.ML	Thu May 11 10:46:52 2023 +0200
+++ b/src/Pure/PIDE/session.ML	Thu May 11 12:20:47 2023 +0200
@@ -11,6 +11,7 @@
   val welcome: unit -> string
   val shutdown: unit -> unit
   val finish: unit -> unit
+  val print_context_tracing: (Context.generic -> bool) -> unit
 end;
 
 structure Session: SESSION =
@@ -43,4 +44,8 @@
   Context.finish_tracing ();
   shutdown ());
 
+fun print_context_tracing pred =
+  List.app (writeln o Proof_Display.print_context_tracing)
+    (filter (pred o #1) (#contexts (Context.finish_tracing ())));
+
 end;