more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;

--- a/src/Doc/Implementation/Logic.thy	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/Doc/Implementation/Logic.thy	Mon Feb 24 20:57:29 2020 +0100
@@ -598,7 +598,7 @@
   \begin{mldecls}
   @{index_ML Theory.add_deps: "Defs.context -> string ->
   Defs.entry -> Defs.entry list -> theory -> theory"} \\
-  @{index_ML Thm_Deps.all_oracles: "thm list -> (string * term option) list"} \\
+  @{index_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Logic.all\<close>~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where
@@ -676,9 +676,10 @@
 
   \<^descr> \<^ML>\<open>Thm_Deps.all_oracles\<close>~\<open>thms\<close> returns all oracles used in the
   internal derivation of the given theorems; this covers the full graph of
-  transitive dependencies. The result contains a name, plus the original
-  proposition, if @{ML Proofterm.proofs} was at least @{ML 1} during the
-  oracle inference. See also the command @{command_ref "thm_oracles"}.
+  transitive dependencies. The result contains an authentic oracle name; if
+  @{ML Proofterm.proofs} was at least @{ML 1} during the oracle inference, it
+  also contains the position of the oracle invocation and its proposition. See
+  also the command @{command_ref "thm_oracles"}.
 \<close>
 
 text %mlantiq \<open>

--- a/src/HOL/ex/Iff_Oracle.thy	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/HOL/ex/Iff_Oracle.thy	Mon Feb 24 20:57:29 2020 +0100
@@ -36,7 +36,7 @@
 ML \<open>iff_oracle (\<^theory>, 10)\<close>
 
 ML \<open>
-  \<^assert> (map #1 (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
+  \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
 \<close>
 
 text \<open>These oracle calls had better fail.\<close>

--- a/src/Pure/General/position.ML	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/Pure/General/position.ML	Mon Feb 24 20:57:29 2020 +0100
@@ -7,6 +7,7 @@
 signature POSITION =
 sig
   eqtype T
+  val ord: T ord
   val make: Thread_Position.T -> T
   val dest: T -> Thread_Position.T
   val line_of: T -> int option
@@ -52,6 +53,7 @@
   val store_reports: report_text list Unsynchronized.ref ->
     T list -> ('a -> Markup.T list) -> 'a -> unit
   val append_reports: report_text list Unsynchronized.ref -> report list -> unit
+  val here_strs: T -> string * string
   val here: T -> string
   val here_list: T list -> string
   type range = T * T
@@ -73,6 +75,19 @@
 
 datatype T = Pos of (int * int * int) * Properties.T;
 
+fun ord (pos1 as Pos ((i, j, k), props), pos2 as Pos ((i', j', k'), props')) =
+  if pointer_eq (pos1, pos2) then EQUAL
+  else
+    (case int_ord (i, i') of
+      EQUAL =>
+        (case int_ord (j, j') of
+          EQUAL =>
+            (case int_ord (k, k') of
+              EQUAL => Properties.ord (props, props')
+            | ord => ord)
+        | ord => ord)
+    | ord => ord);
+
 fun norm_props (props: Properties.T) =
   maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
     Markup.position_properties';
@@ -228,15 +243,17 @@
 
 (* here: user output *)
 
+fun here_strs pos =
+  (case (line_of pos, file_of pos) of
+    (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
+  | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
+  | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
+  | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
+
 fun here pos =
   let
     val props = properties_of pos;
-    val (s1, s2) =
-      (case (line_of pos, file_of pos) of
-        (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
-      | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
-      | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
-      | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
+    val (s1, s2) = here_strs pos;
   in
     if s2 = "" then ""
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2

--- a/src/Pure/General/pretty.ML	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/Pure/General/pretty.ML	Mon Feb 24 20:57:29 2020 +0100
@@ -53,6 +53,7 @@
   val enclose: string -> string -> T list -> T
   val enum: string -> string -> string -> T list -> T
   val position: Position.T -> T
+  val here: Position.T -> T list
   val list: string -> string -> T list -> T
   val str_list: string -> string -> string list -> T
   val big_list: string -> T list -> T
@@ -191,6 +192,15 @@
 val position =
   enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
 
+fun here pos =
+  let
+    val props = Position.properties_of pos;
+    val (s1, s2) = Position.here_strs pos;
+  in
+    if s2 = "" then []
+    else [str s1, mark_str (Markup.properties props Markup.position, s2)]
+  end;
+
 val list = enum ",";
 fun str_list lpar rpar strs = list lpar rpar (map str strs);
 

--- a/src/Pure/General/properties.ML	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/Pure/General/properties.ML	Mon Feb 24 20:57:29 2020 +0100
@@ -8,6 +8,8 @@
 sig
   type entry = string * string
   type T = entry list
+  val entry_ord: entry ord
+  val ord: T ord
   val defined: T -> string -> bool
   val get: T -> string -> string option
   val put: entry -> T -> T
@@ -21,6 +23,9 @@
 type entry = string * string;
 type T = entry list;
 
+val entry_ord = prod_ord string_ord string_ord;
+val ord = list_ord entry_ord;
+
 fun defined (props: T) name = AList.defined (op =) props name;
 fun get (props: T) name = AList.lookup (op =) props name;
 fun put entry (props: T) = AList.update (op =) entry props;

--- a/src/Pure/Proof/extraction.ML	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/Pure/Proof/extraction.ML	Mon Feb 24 20:57:29 2020 +0100
@@ -177,7 +177,7 @@
   let
     val (oracles, thms) =
       ([prf], ([], [])) |-> Proofterm.fold_proof_atoms false
-        (fn Oracle (name, prop, _) => apfst (cons (name, SOME prop))
+        (fn Oracle (name, prop, _) => apfst (cons ((name, Position.none), SOME prop))
           | PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body))
           | _ => I);
     val body =

--- a/src/Pure/proofterm.ML	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/Pure/proofterm.ML	Mon Feb 24 20:57:29 2020 +0100
@@ -26,10 +26,10 @@
    | Oracle of string * term * typ list option
    | PThm of thm_header * thm_body
   and proof_body = PBody of
-    {oracles: (string * term option) Ord_List.T,
+    {oracles: ((string * Position.T) * term option) Ord_List.T,
      thms: (serial * thm_node) Ord_List.T,
      proof: proof}
-  type oracle = string * term option
+  type oracle = (string * Position.T) * term option
   type thm = serial * thm_node
   exception MIN_PROOF of unit
   val proof_of: proof_body -> proof
@@ -218,7 +218,7 @@
  | Oracle of string * term * typ list option
  | PThm of thm_header * thm_body
 and proof_body = PBody of
-  {oracles: (string * term option) Ord_List.T,
+  {oracles: ((string * Position.T) * term option) Ord_List.T,
    thms: (serial * thm_node) Ord_List.T,
    proof: proof}
 and thm_body =
@@ -227,8 +227,9 @@
   Thm_Node of {theory_name: string, name: string, prop: term,
     body: proof_body future, export: unit lazy, consolidate: unit lazy};
 
-type oracle = string * term option;
-val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
+type oracle = (string * Position.T) * term option;
+val oracle_ord: oracle ord =
+  prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord);
 
 type thm = serial * thm_node;
 val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
@@ -374,8 +375,8 @@
       pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
         (map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
 and proof_body consts (PBody {oracles, thms, proof = prf}) =
-  triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts)
-    (oracles, thms, prf)
+  triple (list (pair (pair string (properties o Position.properties_of))
+      (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
 and thm consts (a, thm_node) =
   pair int (pair string (pair string (pair (term consts) (proof_body consts))))
     (a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
@@ -439,7 +440,8 @@
 and proof_body consts x =
   let
     val (a, b, c) =
-      triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) x;
+      triple (list (pair (pair string (Position.of_properties o properties))
+        (option (term consts)))) (list (thm consts)) (proof consts) x;
   in PBody {oracles = a, thms = b, proof = c} end
 and thm consts x =
   let

--- a/src/Pure/thm.ML	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/Pure/thm.ML	Mon Feb 24 20:57:29 2020 +0100
@@ -1065,9 +1065,9 @@
           let
             val (oracle, prf) =
               (case ! Proofterm.proofs of
-                2 => ((name, SOME prop), Proofterm.oracle_proof name prop)
-              | 1 => ((name, SOME prop), MinProof)
-              | 0 => ((name, NONE), MinProof)
+                2 => (((name, Position.thread_data ()), SOME prop), Proofterm.oracle_proof name prop)
+              | 1 => (((name, Position.thread_data ()), SOME prop), MinProof)
+              | 0 => (((name, Position.none), NONE), MinProof)
               | i => bad_proofs i);
           in
             Thm (make_deriv [] [oracle] [] prf,

--- a/src/Pure/thm_deps.ML	Mon Feb 24 12:14:13 2020 +0000
+++ b/src/Pure/thm_deps.ML	Mon Feb 24 20:57:29 2020 +0100
@@ -33,15 +33,15 @@
   in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end;
 
 fun has_skip_proof thms =
-  all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\<open>skip_proof\<close>);
+  all_oracles thms |> exists (fn ((name, _), _) => name = \<^oracle_name>\<open>skip_proof\<close>);
 
 fun pretty_thm_oracles ctxt thms =
   let
     val thy = Proof_Context.theory_of ctxt;
-    fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name]
-      | prt_oracle (name, SOME prop) =
-          [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1,
-            Syntax.pretty_term_global thy prop];
+    fun prt_ora (name, pos) = Thm.pretty_oracle ctxt name :: Pretty.here pos;
+    fun prt_oracle (ora, NONE) = prt_ora ora
+      | prt_oracle (ora, SOME prop) =
+          prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop];
   in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;