# 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;