# HG changeset patch # User wenzelm # Date 1683800447 -7200 # Node ID 73c77db63594a94b0d801734fe2d7239e2e6d621 # Parent a526f69145ec6ed70ac9d8b34c3db9f114eba55f more diagnostic operations; diff -r a526f69145ec -r 73c77db63594 src/Pure/Isar/proof_display.ML --- 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; diff -r a526f69145ec -r 73c77db63594 src/Pure/PIDE/session.ML --- 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;