Facts.Named: include position;
authorwenzelm
Thu Mar 20 16:04:30 2008 +0100 (2008-03-20)
changeset 263617946f459c6c8
parent 26360 cd956c4eadff
child 26362 d9ce159a41d1
Facts.Named: include position;
src/Pure/Isar/attrib.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/spec_parse.ML
src/Pure/ML/ml_context.ML
src/Pure/facts.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Mar 20 12:09:22 2008 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Mar 20 16:04:30 2008 +0100
     1.3 @@ -163,8 +163,8 @@
     1.4    let
     1.5      val thy = Context.theory_of context;
     1.6      val get = Context.cases PureThy.get_fact ProofContext.get_fact context;
     1.7 -    fun get_fact s = get (Facts.Fact s);
     1.8 -    fun get_named s = get (Facts.Named (s, NONE));
     1.9 +    val get_fact = get o Facts.Fact;
    1.10 +    val get_named = get o Facts.named;
    1.11    in
    1.12      Args.$$$ "[" |-- Args.attribs (intern thy) --| Args.$$$ "]" >> (fn srcs =>
    1.13        let
    1.14 @@ -174,8 +174,8 @@
    1.15      ||
    1.16      (Scan.ahead Args.alt_name -- Args.named_fact get_fact
    1.17        >> (fn (s, fact) => ("", Facts.Fact s, fact))
    1.18 -    || Scan.ahead fact_name -- Args.named_fact get_named -- Scan.option Args.thm_sel
    1.19 -      >> (fn ((name, fact), sel) => (name, Facts.Named (name, sel), fact)))
    1.20 +    || Scan.ahead fact_name -- Args.position (Args.named_fact get_named) -- Scan.option Args.thm_sel
    1.21 +      >> (fn ((name, (fact, pos)), sel) => (name, Facts.Named ((name, pos), sel), fact)))
    1.22      -- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
    1.23        let
    1.24          val ths = Facts.select thmref fact;
     2.1 --- a/src/Pure/Isar/find_theorems.ML	Thu Mar 20 12:09:22 2008 +0100
     2.2 +++ b/src/Pure/Isar/find_theorems.ML	Thu Mar 20 16:04:30 2008 +0100
     2.3 @@ -243,7 +243,7 @@
     2.4      EQUAL => (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord)
     2.5    | ord => ord) <> GREATER;
     2.6  
     2.7 -fun nicer (Facts.Named (x, _)) (Facts.Named (y, _)) = nicer_name x y
     2.8 +fun nicer (Facts.Named ((x, _), _)) (Facts.Named ((y, _), _)) = nicer_name x y
     2.9    | nicer (Facts.Fact _) (Facts.Named _) = true
    2.10    | nicer (Facts.Named _) (Facts.Fact _) = false;
    2.11  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 20 12:09:22 2008 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 20 16:04:30 2008 +0100
     3.3 @@ -792,6 +792,8 @@
     3.4  
     3.5  (* get_thm(s) *)
     3.6  
     3.7 +local
     3.8 +
     3.9  fun retrieve_thms _ pick ctxt (Facts.Fact s) =
    3.10        let
    3.11          val prop = Syntax.read_prop (set_mode mode_default ctxt) s
    3.12 @@ -814,19 +816,22 @@
    3.13              | NONE => from_thy thy xthmref);
    3.14        in pick name thms end;
    3.15  
    3.16 -val get_fact_silent = retrieve_thms PureThy.get_fact_silent (K I);
    3.17 +in
    3.18  
    3.19  val get_fact = retrieve_thms PureThy.get_fact (K I);
    3.20  val get_fact_single = retrieve_thms PureThy.get_fact Facts.the_single;
    3.21  
    3.22 -fun get_thms ctxt name = get_fact ctxt (Facts.Named (name, NONE));
    3.23 -fun get_thm ctxt name = get_fact_single ctxt (Facts.Named (name, NONE));
    3.24 +fun get_thms_silent ctxt = retrieve_thms PureThy.get_fact_silent (K I) ctxt o Facts.named;
    3.25 +fun get_thms ctxt = get_fact ctxt o Facts.named;
    3.26 +fun get_thm ctxt = get_fact_single ctxt o Facts.named;
    3.27 +
    3.28 +end;
    3.29  
    3.30  
    3.31  (* valid_thms *)
    3.32  
    3.33  fun valid_thms ctxt (name, ths) =
    3.34 -  (case try (fn () => get_fact_silent ctxt (Facts.Named (name, NONE))) () of
    3.35 +  (case try (fn () => get_thms_silent ctxt name) () of
    3.36      NONE => false
    3.37    | SOME ths' => Thm.eq_thms (ths, ths'));
    3.38  
     4.1 --- a/src/Pure/Isar/proof_display.ML	Thu Mar 20 12:09:22 2008 +0100
     4.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Mar 20 16:04:30 2008 +0100
     4.3 @@ -110,10 +110,8 @@
     4.4            in
     4.5              if a <> "" then ((a, ths), j)
     4.6              else if m = n then ((name, ths), j)
     4.7 -            else if m = 1 then
     4.8 -              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.Single i])), ths), j)
     4.9 -            else
    4.10 -              ((Facts.string_of_ref (Facts.Named (name, SOME [Facts.FromTo (i, j - 1)])), ths), j)
    4.11 +            else ((Facts.string_of_ref (Facts.Named ((name, Position.none),
    4.12 +              SOME ([if m = 1 then Facts.Single i else Facts.FromTo (i, j - 1)]))), ths), j)
    4.13            end;
    4.14        in fst (fold_map name_res res 1) end;
    4.15  
     5.1 --- a/src/Pure/Isar/spec_parse.ML	Thu Mar 20 12:09:22 2008 +0100
     5.2 +++ b/src/Pure/Isar/spec_parse.ML	Thu Mar 20 16:04:30 2008 +0100
     5.3 @@ -70,8 +70,9 @@
     5.4    P.nat >> Facts.Single) --| P.$$$ ")";
     5.5  
     5.6  val xthm =
     5.7 -  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.Named ("", NONE)) ||
     5.8 -  (P.alt_string >> Facts.Fact || P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
     5.9 +  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
    5.10 +  (P.alt_string >> Facts.Fact ||
    5.11 +    P.position P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
    5.12  
    5.13  val xthms1 = Scan.repeat1 xthm;
    5.14  
     6.1 --- a/src/Pure/ML/ml_context.ML	Thu Mar 20 12:09:22 2008 +0100
     6.2 +++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 16:04:30 2008 +0100
     6.3 @@ -275,14 +275,14 @@
     6.4    | print_interval (Facts.From i) = "Facts.From " ^ ML_Syntax.print_int i
     6.5    | print_interval (Facts.Single i) = "Facts.Single " ^ ML_Syntax.print_int i;
     6.6  
     6.7 -fun thm_sel name =
     6.8 +fun thm_sel name_pos =
     6.9    Scan.option Args.thm_sel >> (fn sel => "Facts.Named " ^
    6.10 -    ML_Syntax.print_pair ML_Syntax.print_string
    6.11 -      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name, sel));
    6.12 +    ML_Syntax.print_pair (ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position)
    6.13 +      (ML_Syntax.print_option (ML_Syntax.print_list print_interval)) (name_pos, sel));
    6.14  
    6.15 -fun thm_antiq name get = value_antiq name
    6.16 -  (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel =>
    6.17 -    get ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel));
    6.18 +fun thm_antiq kind get = value_antiq kind
    6.19 +  (Scan.lift (Args.position Args.name :-- thm_sel) >> (fn ((name, _), sel) =>
    6.20 +    (name, get ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel)));
    6.21  
    6.22  in
    6.23  
     7.1 --- a/src/Pure/facts.ML	Thu Mar 20 12:09:22 2008 +0100
     7.2 +++ b/src/Pure/facts.ML	Thu Mar 20 16:04:30 2008 +0100
     7.3 @@ -10,8 +10,9 @@
     7.4    val the_single: string -> thm list -> thm
     7.5    datatype interval = FromTo of int * int | From of int | Single of int
     7.6    datatype ref =
     7.7 -    Named of string * interval list option |
     7.8 +    Named of (string * Position.T) * interval list option |
     7.9      Fact of string
    7.10 +  val named: string -> ref
    7.11    val string_of_ref: ref -> string
    7.12    val name_of_ref: ref -> string
    7.13    val map_name_of_ref: (string -> string) -> ref -> ref
    7.14 @@ -63,17 +64,19 @@
    7.15  (* datatype ref *)
    7.16  
    7.17  datatype ref =
    7.18 -  Named of string * interval list option |
    7.19 +  Named of (string * Position.T) * interval list option |
    7.20    Fact of string;
    7.21  
    7.22 -fun name_of_ref (Named (name, _)) = name
    7.23 +fun named name = Named ((name, Position.none), NONE);
    7.24 +
    7.25 +fun name_of_ref (Named ((name, _), _)) = name
    7.26    | name_of_ref (Fact _) = error "Illegal literal fact";
    7.27  
    7.28 -fun map_name_of_ref f (Named (name, is)) = Named (f name, is)
    7.29 +fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
    7.30    | map_name_of_ref _ r = r;
    7.31  
    7.32 -fun string_of_ref (Named (name, NONE)) = name
    7.33 -  | string_of_ref (Named (name, SOME is)) =
    7.34 +fun string_of_ref (Named ((name, _), NONE)) = name
    7.35 +  | string_of_ref (Named ((name, _), SOME is)) =
    7.36        name ^ enclose "(" ")" (commas (map string_of_interval is))
    7.37    | string_of_ref (Fact _) = error "Illegal literal fact";
    7.38  
    7.39 @@ -82,10 +85,12 @@
    7.40  
    7.41  fun select (Fact _) ths = ths
    7.42    | select (Named (_, NONE)) ths = ths
    7.43 -  | select (Named (name, SOME ivs)) ths =
    7.44 +  | select (Named ((name, pos), SOME ivs)) ths =
    7.45        let
    7.46          val n = length ths;
    7.47 -        fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
    7.48 +        fun err msg =
    7.49 +          error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
    7.50 +            Position.str_of pos);
    7.51          fun sel i =
    7.52            if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
    7.53            else nth ths (i - 1);
    7.54 @@ -95,9 +100,9 @@
    7.55  
    7.56  (* selections *)
    7.57  
    7.58 -fun selections (name, [th]) = [(Named (name, NONE), th)]
    7.59 -  | selections (name, ths) =
    7.60 -      map2 (fn i => fn th => (Named (name, SOME [Single i]), th)) (1 upto length ths) ths;
    7.61 +fun selections (name, [th]) = [(Named ((name, Position.none), NONE), th)]
    7.62 +  | selections (name, ths) = map2 (fn i => fn th =>
    7.63 +      (Named ((name, Position.none), SOME [Single i]), th)) (1 upto length ths) ths;
    7.64  
    7.65  
    7.66  
     8.1 --- a/src/Pure/pure_thy.ML	Thu Mar 20 12:09:22 2008 +0100
     8.2 +++ b/src/Pure/pure_thy.ML	Thu Mar 20 16:04:30 2008 +0100
     8.3 @@ -210,7 +210,7 @@
     8.4  val get_fact_silent = get true;
     8.5  val get_fact = get false;
     8.6  
     8.7 -fun get_thms thy name = get_fact thy (Facts.Named (name, NONE));
     8.8 +fun get_thms thy = get_fact thy o Facts.named;
     8.9  fun get_thm thy name = Facts.the_single name (get_thms thy name);
    8.10  
    8.11  end;