# HG changeset patch
# User wenzelm
# Date 1399558520 -7200
# Node ID 293cd4dcfebca7fc36b48555bb1c09b12eb7731e
# Parent  dc3ba749d3b8ed0edffe71b0eb8c06429e5124c4
some position markup to help locating the query context, e.g. from "Info" dockable;

diff -r dc3ba749d3b8 -r 293cd4dcfebc src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu May 08 15:30:28 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Thu May 08 16:15:20 2014 +0200
@@ -364,8 +364,12 @@
       if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
       else if mode = Backward then Proof_Context.pretty_ctxt ctxt
       else [];
+
+    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
   in
-    [Pretty.str ("proof (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1)),
+    [Pretty.block
+      [Pretty.mark_str (position_markup, "proof"),
+        Pretty.str (" (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2 - 1))],
       Pretty.str ""] @
     (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
     (if verbose orelse mode = Forward then
diff -r dc3ba749d3b8 -r 293cd4dcfebc src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Thu May 08 15:30:28 2014 +0200
+++ b/src/Pure/Tools/find_consts.ML	Thu May 08 16:15:20 2014 +0200
@@ -112,9 +112,13 @@
       fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants []
       |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
       |> map (apsnd fst o snd);
+
+    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
   in
     Pretty.block
-      (Pretty.fbreaks (Pretty.keyword1 "find_consts" :: map pretty_criterion raw_criteria)) ::
+      (Pretty.fbreaks
+        (Pretty.mark position_markup (Pretty.keyword1 "find_consts") ::
+          map pretty_criterion raw_criteria)) ::
     Pretty.str "" ::
     (if null matches then [Pretty.str "found nothing"]
      else
diff -r dc3ba749d3b8 -r 293cd4dcfebc src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu May 08 15:30:28 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Thu May 08 16:15:20 2014 +0200
@@ -482,9 +482,12 @@
             (if returned < found
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
+    val position_markup = Position.markup (Position.thread_data ()) Markup.position;
   in
     Pretty.block
-      (Pretty.fbreaks (Pretty.keyword1 "find_theorems" :: map (pretty_criterion ctxt) criteria)) ::
+      (Pretty.fbreaks
+        (Pretty.mark position_markup (Pretty.keyword1 "find_theorems") ::
+          map (pretty_criterion ctxt) criteria)) ::
     Pretty.str "" ::
     (if null theorems then [Pretty.str "found nothing"]
      else