--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Tue Jun 21 12:10:44 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Tue Jun 21 15:10:43 2016 +0200
@@ -16,7 +16,7 @@
val names = map Thm.get_name_hint thms
val add_info = if null names then I else suffix (":\n" ^ commas names)
- val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
+ val facts = map #1 (Facts.props (Proof_Context.facts_of (Proof.context_of pre)))
fun metis ctxt =
Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jun 21 12:10:44 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Tue Jun 21 15:10:43 2016 +0200
@@ -468,6 +468,7 @@
val named_locals = Facts.dest_static true [global_facts] local_facts
val unnamed_locals =
Facts.props local_facts
+ |> map #1
|> filter (is_useful_unnamed_local_fact ctxt)
|> map (pair "" o single)
--- a/src/Pure/General/binding.ML Tue Jun 21 12:10:44 2016 +0200
+++ b/src/Pure/General/binding.ML Tue Jun 21 15:10:43 2016 +0200
@@ -158,7 +158,7 @@
val print = Pretty.unformatted_string_of o pretty;
-val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o reset_pos);
(* check *)
--- a/src/Pure/Isar/attrib.ML Tue Jun 21 12:10:44 2016 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Jun 21 15:10:43 2016 +0200
@@ -6,21 +6,18 @@
signature ATTRIB =
sig
- type binding = binding * Token.src list
- val empty_binding: binding
- val is_empty_binding: binding -> bool
+ val empty_binding: Attrib.binding
+ val is_empty_binding: Attrib.binding -> bool
val print_attributes: bool -> Proof.context -> unit
- val define_global: Binding.binding -> (Token.src -> attribute) ->
- string -> theory -> string * theory
- val define: Binding.binding -> (Token.src -> attribute) ->
- string -> local_theory -> string * local_theory
+ val define_global: binding -> (Token.src -> attribute) -> string -> theory -> string * theory
+ val define: binding -> (Token.src -> attribute) -> string -> local_theory -> string * local_theory
val check_name_generic: Context.generic -> xstring * Position.T -> string
val check_name: Proof.context -> xstring * Position.T -> string
val check_src: Proof.context -> Token.src -> Token.src
val attribs: Token.src list context_parser
val opt_attribs: Token.src list context_parser
val pretty_attribs: Proof.context -> Token.src list -> Pretty.T list
- val pretty_binding: Proof.context -> binding -> string -> Pretty.T list
+ val pretty_binding: Proof.context -> Attrib.binding -> string -> Pretty.T list
val attribute: Proof.context -> Token.src -> attribute
val attribute_global: theory -> Token.src -> attribute
val attribute_cmd: Proof.context -> Token.src -> attribute
@@ -34,16 +31,16 @@
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
type thms = (thm list * Token.src list) list
- val global_notes: string -> (binding * thms) list ->
+ val global_notes: string -> (Attrib.binding * thms) list ->
theory -> (string * thm list) list * theory
- val local_notes: string -> (binding * thms) list ->
+ val local_notes: string -> (Attrib.binding * thms) list ->
Proof.context -> (string * thm list) list * Proof.context
- val generic_notes: string -> (binding * thms) list ->
+ val generic_notes: string -> (Attrib.binding * thms) list ->
Context.generic -> (string * thm list) list * Context.generic
val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
val attribute_syntax: attribute context_parser -> Token.src -> attribute
- val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
- val local_setup: Binding.binding -> attribute context_parser -> string ->
+ val setup: binding -> attribute context_parser -> string -> theory -> theory
+ val local_setup: binding -> attribute context_parser -> string ->
local_theory -> local_theory
val attribute_setup: bstring * Position.T -> Input.source -> string ->
local_theory -> local_theory
@@ -54,20 +51,17 @@
val thms: thm list context_parser
val multi_thm: thm list context_parser
val transform_facts: morphism -> (Attrib.binding * thms) list -> (Attrib.binding * thms) list
- val partial_evaluation: Proof.context -> (binding * thms) list -> (binding * thms) list
+ val partial_evaluation: Proof.context ->
+ (Attrib.binding * thms) list -> (Attrib.binding * thms) list
val print_options: bool -> Proof.context -> unit
- val config_bool: Binding.binding ->
- (Context.generic -> bool) -> bool Config.T * (theory -> theory)
- val config_int: Binding.binding ->
- (Context.generic -> int) -> int Config.T * (theory -> theory)
- val config_real: Binding.binding ->
- (Context.generic -> real) -> real Config.T * (theory -> theory)
- val config_string: Binding.binding ->
- (Context.generic -> string) -> string Config.T * (theory -> theory)
- val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
- val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
- val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
- val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
+ val config_bool: binding -> (Context.generic -> bool) -> bool Config.T * (theory -> theory)
+ val config_int: binding -> (Context.generic -> int) -> int Config.T * (theory -> theory)
+ val config_real: binding -> (Context.generic -> real) -> real Config.T * (theory -> theory)
+ val config_string: binding -> (Context.generic -> string) -> string Config.T * (theory -> theory)
+ val setup_config_bool: binding -> (Context.generic -> bool) -> bool Config.T
+ val setup_config_int: binding -> (Context.generic -> int) -> int Config.T
+ val setup_config_real: binding -> (Context.generic -> real) -> real Config.T
+ val setup_config_string: binding -> (Context.generic -> string) -> string Config.T
val option_bool: string * Position.T -> bool Config.T * (theory -> theory)
val option_int: string * Position.T -> int Config.T * (theory -> theory)
val option_real: string * Position.T -> real Config.T * (theory -> theory)
@@ -83,12 +77,12 @@
val case_conclusion: string * string list -> Token.src
end;
-structure Attrib: ATTRIB =
+structure Attrib: sig type binding = Attrib.binding include ATTRIB end =
struct
(* source and bindings *)
-type binding = binding * Token.src list;
+type binding = Attrib.binding;
val empty_binding: binding = (Binding.empty, []);
fun is_empty_binding ((b, srcs): binding) = Binding.is_empty b andalso null srcs;
--- a/src/Pure/Isar/proof_context.ML Tue Jun 21 12:10:44 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Jun 21 15:10:43 2016 +0200
@@ -945,15 +945,18 @@
in
-fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
-
fun potential_facts ctxt prop =
let
val body = Term.strip_all_body prop;
- val vacuous = filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts;
+ val vacuous =
+ filter (fn th => Term.could_unify (body, Thm.concl_of th)) vacuous_facts
+ |> map (rpair Position.none);
in Facts.could_unify (facts_of ctxt) body @ vacuous end;
-fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i);
+fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts;
+
+fun some_fact_tac ctxt =
+ SUBGOAL (fn (goal, i) => fact_tac ctxt (map #1 (potential_facts ctxt goal)) i);
end;
@@ -993,18 +996,23 @@
val prop =
Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
|> singleton (Variable.polymorphic ctxt);
- fun err msg = error (msg ^ Position.here pos ^ ":\n" ^ Syntax.string_of_term ctxt prop);
+ fun err ps msg =
+ error (msg ^ Position.here_list (pos :: ps) ^ ":\n" ^ Syntax.string_of_term ctxt prop);
val (prop', _) = Term.replace_dummy_patterns prop (Variable.maxidx_of ctxt + 1);
- fun prove_fact th =
- Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
- val results = map_filter (try prove_fact) (potential_facts ctxt prop');
- val thm =
- (case distinct Thm.eq_thm_prop results of
- [thm] => thm
- | [] => err "Failed to retrieve literal fact"
- | _ => err "Ambiguous specification of literal fact");
- in pick true ("", Position.none) [thm] end
+ fun prove th = Goal.prove ctxt [] [] prop' (K (ALLGOALS (fact_tac ctxt [th])));
+ val results = map_filter (try (apfst prove)) (potential_facts ctxt prop');
+ val (thm, thm_pos) =
+ (case distinct (eq_fst Thm.eq_thm_prop) results of
+ [res] => res
+ | [] => err [] "Failed to retrieve literal fact"
+ | dups => err (distinct (op =) (map #2 dups)) "Ambiguous specification of literal fact");
+
+ val markup =
+ (Markup.entity Markup.literal_factN "")
+ |> Markup.properties (Position.def_properties_of thm_pos);
+ val _ = Context_Position.report_generic context pos markup;
+ in pick true ("", thm_pos) [thm] end
| retrieve pick context (Facts.Named ((xname, pos), sel)) =
let
val thy = Context.theory_of context;
@@ -1450,7 +1458,7 @@
fun pretty_local_facts verbose ctxt =
let
val facts = facts_of ctxt;
- val props = Facts.props facts;
+ val props = map #1 (Facts.props facts);
val local_facts =
(if null props then [] else [("<unnamed>", props)]) @
Facts.dest_static verbose [Global_Theory.facts_of (theory_of ctxt)] facts;
--- a/src/Pure/PIDE/markup.ML Tue Jun 21 12:10:44 2016 +0200
+++ b/src/Pure/PIDE/markup.ML Tue Jun 21 15:10:43 2016 +0200
@@ -86,6 +86,7 @@
val fixedN: string val fixed: string -> T
val caseN: string val case_: string -> T
val dynamic_factN: string val dynamic_fact: string -> T
+ val literal_factN: string val literal_fact: string -> T
val method_modifierN: string
val tfreeN: string val tfree: T
val tvarN: string val tvar: T
@@ -343,7 +344,9 @@
val (bindingN, binding) = markup_elem "binding";
val entityN = "entity";
-fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
+fun entity kind name =
+ (entityN,
+ (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
fun get_entity_kind (name, props) =
if name = entityN then AList.lookup (op =) props kindN
@@ -441,6 +444,7 @@
val (fixedN, fixed) = markup_string "fixed" nameN;
val (caseN, case_) = markup_string "case" nameN;
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
+val (literal_factN, literal_fact) = markup_string "literal_fact" nameN;
val method_modifierN = "method_modifier";
--- a/src/Pure/PIDE/markup.scala Tue Jun 21 12:10:44 2016 +0200
+++ b/src/Pure/PIDE/markup.scala Tue Jun 21 15:10:43 2016 +0200
@@ -95,10 +95,9 @@
def unapply(markup: Markup): Option[(String, String)] =
markup match {
case Markup(ENTITY, props) =>
- (props, props) match {
- case (Kind(kind), Name(name)) => Some((kind, name))
- case _ => None
- }
+ val kind = Kind.unapply(props).getOrElse("")
+ val name = Name.unapply(props).getOrElse("")
+ Some((kind, name))
case _ => None
}
}
--- a/src/Pure/facts.ML Tue Jun 21 12:10:44 2016 +0200
+++ b/src/Pure/facts.ML Tue Jun 21 15:10:43 2016 +0200
@@ -36,8 +36,8 @@
val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
val dest_static: bool -> T list -> T -> (string * thm list) list
val dest_all: Context.generic -> bool -> T list -> T -> (string * thm list) list
- val props: T -> thm list
- val could_unify: T -> term -> thm list
+ val props: T -> (thm * Position.T) list
+ val could_unify: T -> term -> (thm * Position.T) list
val merge: T * T -> T
val add_static: Context.generic -> {strict: bool, index: bool} ->
binding * thm list -> T -> string * T
@@ -134,7 +134,7 @@
datatype T = Facts of
{facts: fact Name_Space.table,
- props: thm Net.net};
+ props: (thm * Position.T) Net.net};
fun make_facts facts props = Facts {facts = facts, props = props};
@@ -227,7 +227,7 @@
(* indexed props *)
-val prop_ord = Term_Ord.term_ord o apply2 Thm.full_prop_of;
+val prop_ord = Term_Ord.term_ord o apply2 (Thm.full_prop_of o fst);
fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props);
fun could_unify (Facts {props, ...}) = Net.unify_term props;
@@ -250,11 +250,13 @@
fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
let
val ths' = map Thm.trim_context ths;
+ val pos = #2 (Position.default (Binding.pos_of b));
+
val (name, facts') =
if Binding.is_empty b then ("", facts)
else Name_Space.define context strict (b, Static ths') facts;
val props' = props
- |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths';
+ |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, (th, pos))) ths';
in (name, make_facts facts' props') end;
--- a/src/Tools/jEdit/src/rendering.scala Tue Jun 21 12:10:44 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Tue Jun 21 15:10:43 2016 +0200
@@ -604,6 +604,7 @@
val kind1 = Word.implode(Word.explode('_', kind))
val txt1 =
if (name == "") kind1
+ else if (kind1 == "") quote(name)
else kind1 + " " + quote(name)
val t = prev.info._1
val txt2 =