# HG changeset patch
# User wenzelm
# Date 1408026014 -7200
# Node ID e5bec882fdd0cd45ff85085c0e853266a28a3714
# Parent  57200bdc2aa78072059ea86e1adbeccab5d656ea
more informative Token.Fact: retain name of dynamic fact (without selection);

diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Aug 14 14:28:11 2014 +0200
+++ b/src/Pure/Isar/args.ML	Thu Aug 14 16:20:14 2014 +0200
@@ -51,7 +51,7 @@
   val named_text: (string -> string) -> string parser
   val named_typ: (string -> typ) -> typ parser
   val named_term: (string -> term) -> term parser
-  val named_fact: (string -> thm list) -> thm list parser
+  val named_fact: (string -> string option * thm list) -> thm list parser
   val named_attribute:
     (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
   val typ_abbrev: typ context_parser
@@ -106,7 +106,7 @@
       | SOME (Token.Text s) => Pretty.str (quote s)
       | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
       | SOME (Token.Term t) => Syntax.pretty_term ctxt t
-      | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
+      | SOME (Token.Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
       | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
   in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
 
@@ -130,7 +130,7 @@
 fun transform_values phi = map_args (Token.map_value
   (fn Token.Typ T => Token.Typ (Morphism.typ phi T)
     | Token.Term t => Token.Term (Morphism.term phi t)
-    | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
+    | Token.Fact (a, ths) => Token.Fact (a, Morphism.fact phi ths)
     | Token.Attribute att => Token.Attribute (Morphism.transform phi att)
     | tok => tok));
 
@@ -212,15 +212,17 @@
 val internal_text = value (fn Token.Text s => s);
 val internal_typ = value (fn Token.Typ T => T);
 val internal_term = value (fn Token.Term t => t);
-val internal_fact = value (fn Token.Fact ths => ths);
+val internal_fact = value (fn Token.Fact (_, ths) => ths);
 val internal_attribute = value (fn Token.Attribute att => att);
 
 fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
 fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
 fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
 
-fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
-  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of);
+fun named_fact get =
+  internal_fact ||
+  named >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
+  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2;
 
 fun named_attribute att =
   internal_attribute ||
diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Aug 14 14:28:11 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 16:20:14 2014 +0200
@@ -245,7 +245,9 @@
   let
     val get = Proof_Context.get_fact_generic context;
     val get_fact = get o Facts.Fact;
-    fun get_named pos name = get (Facts.Named ((name, pos), NONE));
+    fun get_named is_sel pos name =
+      let val (a, ths) = get (Facts.Named ((name, pos), NONE))
+      in (if is_sel then NONE else a, ths) end;
   in
     Parse.$$$ "[" |-- Args.attribs (check_name_generic context) --| Parse.$$$ "]" >> (fn srcs =>
       let
@@ -255,9 +257,9 @@
     ||
     (Scan.ahead Args.alt_name -- Args.named_fact get_fact
       >> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
-     Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
-      Args.named_fact (get_named pos) -- Scan.option thm_sel
-        >> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
+     Scan.ahead (Parse.position fact_name -- Scan.option thm_sel) :|-- (fn ((name, pos), sel) =>
+      Args.named_fact (get_named (is_some sel) pos) --| Scan.option thm_sel
+        >> (fn fact => (name, Facts.Named ((name, pos), sel), fact))))
     -- Args.opt_attribs (check_name_generic context) >> (fn ((name, thmref, fact), srcs) =>
       let
         val ths = Facts.select thmref fact;
diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Aug 14 14:28:11 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 14 16:20:14 2014 +0200
@@ -121,7 +121,7 @@
     (term list list * (Proof.context -> Proof.context)) * Proof.context
   val fact_tac: Proof.context -> thm list -> int -> tactic
   val some_fact_tac: Proof.context -> int -> tactic
-  val get_fact_generic: Context.generic -> Facts.ref -> thm list
+  val get_fact_generic: Context.generic -> Facts.ref -> string option * thm list
   val get_fact: Proof.context -> Facts.ref -> thm list
   val get_fact_single: Proof.context -> Facts.ref -> thm
   val get_thms: Proof.context -> xstring -> thm list
@@ -948,22 +948,27 @@
             [thm] => thm
           | [] => err "Failed to retrieve literal fact"
           | _ => err "Ambiguous specification of literal fact");
-      in pick ("", Position.none) [thm] end
-  | retrieve pick context (Facts.Named ((xname, pos), ivs)) =
+      in pick true ("", Position.none) [thm] end
+  | retrieve pick context (Facts.Named ((xname, pos), sel)) =
       let
         val thy = Context.theory_of context;
-        val (name, thms) =
+        fun immediate thm = {name = xname, static = true, thms = [Thm.transfer thy thm]};
+        val {name, static, thms} =
           (case xname of
-            "" => (xname, [Thm.transfer thy Drule.dummy_thm])
-          | "_" => (xname, [Thm.transfer thy Drule.asm_rl])
+            "" => immediate Drule.dummy_thm
+          | "_" => immediate Drule.asm_rl
           | _ => retrieve_generic context (xname, pos));
-      in pick (name, pos) (Facts.select (Facts.Named ((name, pos), ivs)) thms) end;
+        val thms' = Facts.select (Facts.Named ((name, pos), sel)) thms;
+      in pick (static orelse is_some sel) (name, pos) thms' end;
 
 in
 
-val get_fact_generic = retrieve (K I);
-val get_fact = retrieve (K I) o Context.Proof;
-val get_fact_single = retrieve Facts.the_single o Context.Proof;
+val get_fact_generic =
+  retrieve (fn static => fn (name, _) => fn thms =>
+    (if static then NONE else SOME name, thms));
+
+val get_fact = retrieve (K (K I)) o Context.Proof;
+val get_fact_single = retrieve (K Facts.the_single) o Context.Proof;
 
 fun get_thms ctxt = get_fact ctxt o Facts.named;
 fun get_thm ctxt = get_fact_single ctxt o Facts.named;
diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Aug 14 14:28:11 2014 +0200
+++ b/src/Pure/Isar/token.ML	Thu Aug 14 16:20:14 2014 +0200
@@ -12,7 +12,8 @@
     Error of string | Sync | EOF
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   datatype value =
-    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
+    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term |
+    Fact of string option * thm list |
     Attribute of morphism -> attribute | Files of file Exn.result list
   type T
   val str_of_kind: kind -> string
@@ -57,7 +58,7 @@
   val mk_text: string -> T
   val mk_typ: typ -> T
   val mk_term: term -> T
-  val mk_fact: thm list -> T
+  val mk_fact: string option * thm list -> T
   val mk_attribute: (morphism -> attribute) -> T
   val init_assignable: T -> T
   val assign: value option -> T -> unit
@@ -91,7 +92,7 @@
   Text of string |
   Typ of typ |
   Term of term |
-  Fact of thm list |
+  Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
   Attribute of morphism -> attribute |
   Files of file Exn.result list;
 
diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Thu Aug 14 14:28:11 2014 +0200
+++ b/src/Pure/facts.ML	Thu Aug 14 16:20:14 2014 +0200
@@ -29,7 +29,8 @@
   val extern: Proof.context -> T -> string -> xstring
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
-  val retrieve: Context.generic -> T -> xstring * Position.T -> string * thm list
+  val retrieve: Context.generic -> T -> xstring * Position.T ->
+    {name: string, static: bool, thms: thm list}
   val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: bool -> T list -> T -> (string * thm list) list
@@ -176,14 +177,18 @@
 fun retrieve context facts (xname, pos) =
   let
     val name = check context facts (xname, pos);
-    val thms =
+    val (static, thms) =
       (case lookup context facts name of
         SOME (static, thms) =>
           (if static then ()
            else Context_Position.report_generic context pos (Markup.dynamic_fact name);
-           thms)
+           (static, thms))
       | NONE => error ("Unknown fact " ^ quote name ^ Position.here pos));
-  in (name, map (Thm.transfer (Context.theory_of context)) thms) end;
+  in
+   {name = name,
+    static = static,
+    thms = map (Thm.transfer (Context.theory_of context)) thms}
+  end;
 
 
 (* static content *)
diff -r 57200bdc2aa7 -r e5bec882fdd0 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Thu Aug 14 14:28:11 2014 +0200
+++ b/src/Pure/global_theory.ML	Thu Aug 14 16:20:14 2014 +0200
@@ -72,7 +72,7 @@
 (* retrieve theorems *)
 
 fun get_thms thy xname =
-  #2 (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
+  #thms (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none));
 
 fun get_thm thy xname =
   Facts.the_single (xname, Position.none) (get_thms thy xname);