# HG changeset patch
# User wenzelm
# Date 1466514643 -7200
# Node ID 94c6e3ed0afb151a54dc5a7473226d88f38217a5
# Parent  bd37a72a940ada891eff07b3d07805886c6f1567# Parent  ae9330fdbc16fe443840244c0a5f0f467551fb31
merged

diff -r bd37a72a940a -r 94c6e3ed0afb src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- 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
diff -r bd37a72a940a -r 94c6e3ed0afb src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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)
 
diff -r bd37a72a940a -r 94c6e3ed0afb src/Pure/General/binding.ML
--- 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 *)
diff -r bd37a72a940a -r 94c6e3ed0afb src/Pure/Isar/attrib.ML
--- 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;
diff -r bd37a72a940a -r 94c6e3ed0afb src/Pure/Isar/proof_context.ML
--- 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;
diff -r bd37a72a940a -r 94c6e3ed0afb src/Pure/PIDE/markup.ML
--- 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";
 
diff -r bd37a72a940a -r 94c6e3ed0afb src/Pure/PIDE/markup.scala
--- 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
       }
   }
diff -r bd37a72a940a -r 94c6e3ed0afb src/Pure/facts.ML
--- 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;
 
 
diff -r bd37a72a940a -r 94c6e3ed0afb src/Tools/jEdit/src/rendering.scala
--- 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 =