# HG changeset patch
# User wenzelm
# Date 1206025470 -3600
# Node ID 7946f459c6c87099d4fed551b691e7139e399d81
# Parent  cd956c4eadff9b166a5fcec4b4d9b25eb2a668ed
Facts.Named: include position;

diff -r cd956c4eadff -r 7946f459c6c8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Mar 20 12:09:22 2008 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Mar 20 16:04:30 2008 +0100
@@ -163,8 +163,8 @@
   let
     val thy = Context.theory_of context;
     val get = Context.cases PureThy.get_fact ProofContext.get_fact context;
-    fun get_fact s = get (Facts.Fact s);
-    fun get_named s = get (Facts.Named (s, NONE));
+    val get_fact = get o Facts.Fact;
+    val get_named = get o Facts.named;
   in
     Args.$$$ "[" |-- Args.attribs (intern thy) --| Args.$$$ "]" >> (fn srcs =>
       let
@@ -174,8 +174,8 @@
     ||
     (Scan.ahead Args.alt_name -- Args.named_fact get_fact
       >> (fn (s, fact) => ("", Facts.Fact s, fact))
-    || Scan.ahead fact_name -- Args.named_fact get_named -- Scan.option Args.thm_sel
-      >> (fn ((name, fact), sel) => (name, Facts.Named (name, sel), fact)))
+    || Scan.ahead fact_name -- Args.position (Args.named_fact get_named) -- Scan.option Args.thm_sel
+      >> (fn ((name, (fact, pos)), sel) => (name, Facts.Named ((name, pos), sel), fact)))
     -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
       let
         val ths = Facts.select thmref fact;
diff -r cd956c4eadff -r 7946f459c6c8 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Thu Mar 20 12:09:22 2008 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Thu Mar 20 16:04:30 2008 +0100
@@ -243,7 +243,7 @@
     EQUAL => (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
   | ord => ord) <> GREATER;
 
-fun nicer (Facts.Named (x, _)) (Facts.Named (y, _)) = nicer_name x y
+fun nicer (Facts.Named ((x, _), _)) (Facts.Named ((y, _), _)) = nicer_name x y
   | nicer (Facts.Fact _) (Facts.Named _) = true
   | nicer (Facts.Named _) (Facts.Fact _) = false;
 
diff -r cd956c4eadff -r 7946f459c6c8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 20 12:09:22 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 20 16:04:30 2008 +0100
@@ -792,6 +792,8 @@
 
 (* get_thm(s) *)
 
+local
+
 fun retrieve_thms _ pick ctxt (Facts.Fact s) =
       let
         val prop = Syntax.read_prop (set_mode mode_default ctxt) s
@@ -814,19 +816,22 @@
             | NONE => from_thy thy xthmref);
       in pick name thms end;
 
-val get_fact_silent = retrieve_thms PureThy.get_fact_silent (K I);
+in
 
 val get_fact = retrieve_thms PureThy.get_fact (K I);
 val get_fact_single = retrieve_thms PureThy.get_fact Facts.the_single;
 
-fun get_thms ctxt name = get_fact ctxt (Facts.Named (name, NONE));
-fun get_thm ctxt name = get_fact_single ctxt (Facts.Named (name, NONE));
+fun get_thms_silent ctxt = retrieve_thms PureThy.get_fact_silent (K I) ctxt o Facts.named;
+fun get_thms ctxt = get_fact ctxt o Facts.named;
+fun get_thm ctxt = get_fact_single ctxt o Facts.named;
+
+end;
 
 
 (* valid_thms *)
 
 fun valid_thms ctxt (name, ths) =
-  (case try (fn () => get_fact_silent ctxt (Facts.Named (name, NONE))) () of
+  (case try (fn () => get_thms_silent ctxt name) () of
     NONE => false
   | SOME ths' => Thm.eq_thms (ths, ths'));
 
diff -r cd956c4eadff -r 7946f459c6c8 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Thu Mar 20 12:09:22 2008 +0100
+++ b/src/Pure/Isar/proof_display.ML	Thu Mar 20 16:04:30 2008 +0100
@@ -110,10 +110,8 @@
           in
             if a <> "" then ((a, ths), j)
             else if m = n then ((name, ths), j)
-            else if m = 1 then
-              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.Single i])), ths), j)
-            else
-              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.FromTo (i, j - 1)])), ths), j)
+            else ((Facts.string_of_ref (Facts.Named ((name, Position.none),
+              SOME ([if m = 1 then Facts.Single i else Facts.FromTo (i, j - 1)]))), ths), j)
           end;
       in fst (fold_map name_res res 1) end;
 
diff -r cd956c4eadff -r 7946f459c6c8 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Thu Mar 20 12:09:22 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Thu Mar 20 16:04:30 2008 +0100
@@ -70,8 +70,9 @@
   P.nat >> Facts.Single) --| P.$$$ ")";
 
 val xthm =
-  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.Named ("", NONE)) ||
-  (P.alt_string >> Facts.Fact || P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
+  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
+  (P.alt_string >> Facts.Fact ||
+    P.position P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
 
 val xthms1 = Scan.repeat1 xthm;
 
diff -r cd956c4eadff -r 7946f459c6c8 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 20 12:09:22 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 16:04:30 2008 +0100
@@ -275,14 +275,14 @@
   | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i
   | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
 
-fun thm_sel name =
+fun thm_sel name_pos =
   Scan.option Args.thm_sel >> (fn sel => "Facts.Named " ^
-    ML_Syntax.print_pair ML_Syntax.print_string
-      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name, sel));
+    ML_Syntax.print_pair (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position)
+      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name_pos, sel));
 
-fun thm_antiq name get = value_antiq name
-  (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel =>
-    get ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel));
+fun thm_antiq kind get = value_antiq kind
+  (Scan.lift (Args.position Args.name :-- thm_sel) >> (fn ((name, _), sel) =>
+    (name, get ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel)));
 
 in
 
diff -r cd956c4eadff -r 7946f459c6c8 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Thu Mar 20 12:09:22 2008 +0100
+++ b/src/Pure/facts.ML	Thu Mar 20 16:04:30 2008 +0100
@@ -10,8 +10,9 @@
   val the_single: string -> thm list -> thm
   datatype interval = FromTo of int * int | From of int | Single of int
   datatype ref =
-    Named of string * interval list option |
+    Named of (string * Position.T) * interval list option |
     Fact of string
+  val named: string -> ref
   val string_of_ref: ref -> string
   val name_of_ref: ref -> string
   val map_name_of_ref: (string -> string) -> ref -> ref
@@ -63,17 +64,19 @@
 (* datatype ref *)
 
 datatype ref =
-  Named of string * interval list option |
+  Named of (string * Position.T) * interval list option |
   Fact of string;
 
-fun name_of_ref (Named (name, _)) = name
+fun named name = Named ((name, Position.none), NONE);
+
+fun name_of_ref (Named ((name, _), _)) = name
   | name_of_ref (Fact _) = error "Illegal literal fact";
 
-fun map_name_of_ref f (Named (name, is)) = Named (f name, is)
+fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
   | map_name_of_ref _ r = r;
 
-fun string_of_ref (Named (name, NONE)) = name
-  | string_of_ref (Named (name, SOME is)) =
+fun string_of_ref (Named ((name, _), NONE)) = name
+  | string_of_ref (Named ((name, _), SOME is)) =
       name ^ enclose "(" ")" (commas (map string_of_interval is))
   | string_of_ref (Fact _) = error "Illegal literal fact";
 
@@ -82,10 +85,12 @@
 
 fun select (Fact _) ths = ths
   | select (Named (_, NONE)) ths = ths
-  | select (Named (name, SOME ivs)) ths =
+  | select (Named ((name, pos), SOME ivs)) ths =
       let
         val n = length ths;
-        fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
+        fun err msg =
+          error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
+            Position.str_of pos);
         fun sel i =
           if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
           else nth ths (i - 1);
@@ -95,9 +100,9 @@
 
 (* selections *)
 
-fun selections (name, [th]) = [(Named (name, NONE), th)]
-  | selections (name, ths) =
-      map2 (fn i => fn th => (Named (name, SOME [Single i]), th)) (1 upto length ths) ths;
+fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
+  | selections (name, ths) = map2 (fn i => fn th =>
+      (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
 
 
 
diff -r cd956c4eadff -r 7946f459c6c8 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Mar 20 12:09:22 2008 +0100
+++ b/src/Pure/pure_thy.ML	Thu Mar 20 16:04:30 2008 +0100
@@ -210,7 +210,7 @@
 val get_fact_silent = get true;
 val get_fact = get false;
 
-fun get_thms thy name = get_fact thy (Facts.Named (name, NONE));
+fun get_thms thy = get_fact thy o Facts.named;
 fun get_thm thy name = Facts.the_single name (get_thms thy name);
 
 end;