more position markup to help locating the query context, e.g. from "Info" dockable;

--- a/src/HOL/Tools/Function/function.ML	Fri May 09 21:03:44 2014 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri May 09 22:04:50 2014 +0200
@@ -132,7 +132,9 @@
           fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
           pelims=pelims',elims=NONE}
 
-        val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
+        val _ =
+          Proof_Display.print_consts do_print (Position.thread_data ()) lthy
+            (K false) (map fst fixes)
       in
         (info,
          lthy |> Local_Theory.declaration {syntax = false, pervasive = false}

--- a/src/Pure/Isar/obtain.ML	Fri May 09 21:03:44 2014 +0200
+++ b/src/Pure/Isar/obtain.ML	Fri May 09 22:04:50 2014 +0200
@@ -299,8 +299,9 @@
       end;
 
     val goal = Var (("guess", 0), propT);
+    val pos = Position.thread_data ();
     fun print_result ctxt' (k, [(s, [_, th])]) =
-      Proof_Display.print_results int ctxt' (k, [(s, [th])]);
+      Proof_Display.print_results int pos ctxt' (k, [(s, [th])]);
     val before_qed =
       Method.primitive_text (fn ctxt =>
         Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>

--- a/src/Pure/Isar/proof.ML	Fri May 09 21:03:44 2014 +0200
+++ b/src/Pure/Isar/proof.ML	Fri May 09 22:04:50 2014 +0200
@@ -1045,7 +1045,7 @@
 local
 
 fun gen_have prep_att prepp before_qed after_qed stmt int =
-  local_goal (Proof_Display.print_results int)
+  local_goal (Proof_Display.print_results int (Position.thread_data ()))
     prep_att prepp "have" before_qed after_qed stmt;
 
 fun gen_show prep_att prepp before_qed after_qed stmt int state =
@@ -1057,9 +1057,10 @@
       (case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
       |> cat_lines;
 
+    val pos = Position.thread_data ();
     fun print_results ctxt res =
       if ! testing then ()
-      else Proof_Display.print_results int ctxt res;
+      else Proof_Display.print_results int pos ctxt res;
     fun print_rule ctxt th =
       if ! testing then rule := SOME th
       else if int then

--- a/src/Pure/Isar/proof_display.ML	Fri May 09 21:03:44 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML	Fri May 09 22:04:50 2014 +0200
@@ -22,8 +22,10 @@
   val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
   val method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
-  val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
-  val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
+  val print_results: bool -> Position.T -> Proof.context ->
+    ((string * string) * (string * thm list) list) -> unit
+  val print_consts: bool -> Position.T -> Proof.context ->
+    (string * typ -> bool) -> (string * typ) list -> unit
 end
 
 structure Proof_Display: PROOF_DISPLAY =
@@ -127,11 +129,13 @@
 
 (* results *)
 
+fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
+
 local
 
-fun pretty_fact_name (kind, "") = Pretty.keyword1 kind
-  | pretty_fact_name (kind, name) =
-      Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
+fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
+  | pretty_fact_name pos (kind, name) =
+      Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1,
         Pretty.str (Long_Name.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
@@ -140,17 +144,18 @@
 
 in
 
-fun print_results do_print ctxt ((kind, name), facts) =
+fun print_results do_print pos ctxt ((kind, name), facts) =
   if not do_print orelse kind = "" then ()
   else if name = "" then
     (Pretty.writeln o Pretty.mark Markup.state)
-      (Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
+      (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
+        pretty_facts ctxt facts))
   else
     (Pretty.writeln o Pretty.mark Markup.state)
       (case facts of
-        [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
+        [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
           Proof_Context.pretty_fact ctxt fact])
-      | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
+      | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
           Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
 
 end;
@@ -164,18 +169,19 @@
   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
     Pretty.quote (Syntax.pretty_typ ctxt T)];
 
-fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
+fun pretty_vars pos ctxt kind vs =
+  Pretty.block (Pretty.fbreaks (position_markup pos (Pretty.str kind) :: map (pretty_var ctxt) vs));
 
-fun pretty_consts ctxt pred cs =
+fun pretty_consts pos ctxt pred cs =
   (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
-    [] => pretty_vars ctxt "constants" cs
-  | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]);
+    [] => pretty_vars pos ctxt "constants" cs
+  | ps => Pretty.chunks [pretty_vars pos ctxt "parameters" ps, pretty_vars pos ctxt "constants" cs]);
 
 in
 
-fun print_consts do_print ctxt pred cs =
+fun print_consts do_print pos ctxt pred cs =
   if not do_print orelse null cs then ()
-  else Pretty.writeln (Pretty.mark Markup.state (pretty_consts ctxt pred cs));
+  else Pretty.writeln (Pretty.mark Markup.state (pretty_consts pos ctxt pred cs));
 
 end;
 

--- a/src/Pure/Isar/specification.ML	Fri May 09 21:03:44 2014 +0200
+++ b/src/Pure/Isar/specification.ML	Fri May 09 22:04:50 2014 +0200
@@ -223,7 +223,9 @@
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
 
-    val _ = Proof_Display.print_consts int lthy4 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
+    val _ =
+      Proof_Display.print_consts int (Position.thread_data ()) lthy4
+        (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   in ((lhs, (def_name, th')), lthy4) end;
 
 val definition' = gen_def check_free_spec;
@@ -256,7 +258,7 @@
       |> Local_Theory.abbrev mode (var, rhs) |> snd
       |> Proof_Context.restore_syntax_mode lthy;
 
-    val _ = Proof_Display.print_consts int lthy2 (K false) [(x, T)];
+    val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
   in lthy2 end;
 
 val abbreviation = gen_abbrev check_free_spec;
@@ -301,7 +303,7 @@
       |> Attrib.partial_evaluation ctxt'
       |> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
     val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
-    val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
+    val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res);
   in (res, lthy') end;
 
 in
@@ -389,6 +391,7 @@
       |> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
     val atts = more_atts @ map (prep_att lthy) raw_atts;
 
+    val pos = Position.thread_data ();
     fun after_qed' results goal_ctxt' =
       let
         val results' =
@@ -400,12 +403,12 @@
               (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
         val lthy'' =
           if Attrib.is_empty_binding (name, atts) then
-            (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
+            (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy')
           else
             let
               val ([(res_name, _)], lthy'') =
                 Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
-              val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
+              val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res);
             in lthy'' end;
       in after_qed results' lthy'' end;
   in