# HG changeset patch
# User wenzelm
# Date 1303066723 -7200
# Node ID d9fe47d21b41efd490a5f7a503a8b47fba9631ed
# Parent  c113db12bf8b91fbb07b8b84549b99fa05c41e7a
markup facts via name space;
eliminated obsolete markup;

diff -r c113db12bf8b -r d9fe47d21b41 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Apr 17 20:25:10 2011 +0200
+++ b/src/Pure/General/markup.ML	Sun Apr 17 20:58:43 2011 +0200
@@ -39,9 +39,7 @@
   val fixed_declN: string val fixed_decl: string -> T
   val fixedN: string val fixed: string -> T
   val constN: string val const: string -> T
-  val factN: string val fact: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
-  val local_factN: string val local_fact: string -> T
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
   val freeN: string val free: T
@@ -216,9 +214,7 @@
 val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (constN, const) = markup_string "constant" nameN;
-val (factN, fact) = markup_string "fact" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
-val (local_factN, local_fact) = markup_string "local_fact" nameN;
 
 
 (* inner syntax *)
diff -r c113db12bf8b -r d9fe47d21b41 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun Apr 17 20:25:10 2011 +0200
+++ b/src/Pure/General/markup.scala	Sun Apr 17 20:58:43 2011 +0200
@@ -152,9 +152,7 @@
   val FIXED_DECL = "fixed_decl"
   val FIXED = "fixed"
   val CONST = "constant"
-  val FACT = "fact"
   val DYNAMIC_FACT = "dynamic_fact"
-  val LOCAL_FACT = "local_fact"
 
 
   /* inner syntax */
diff -r c113db12bf8b -r d9fe47d21b41 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 20:25:10 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Apr 17 20:58:43 2011 +0200
@@ -324,23 +324,26 @@
 
 (* extern *)
 
-fun extern_fact ctxt name =
+fun which_facts ctxt name =
   let
     val local_facts = facts_of ctxt;
     val global_facts = Global_Theory.facts_of (theory_of ctxt);
   in
     if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
-    then Facts.extern ctxt local_facts name
-    else Facts.extern ctxt global_facts name
+    then local_facts else global_facts
   end;
 
+fun markup_fact ctxt name = Name_Space.markup_entry (Facts.space_of (which_facts ctxt name)) name;
+
+fun extern_fact ctxt name = Facts.extern ctxt (which_facts ctxt name) name;
+
 
 (* pretty *)
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
-fun pretty_fact_name ctxt a = Pretty.block
-  [Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"];
+fun pretty_fact_name ctxt a =
+  Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
 
 fun pretty_fact_aux ctxt flag ("", ths) =
       Display.pretty_thms_aux ctxt flag ths
@@ -884,8 +887,9 @@
           else
             (case Facts.lookup (Context.Proof ctxt) local_facts name of
               SOME (_, ths) =>
-               (Context_Position.report ctxt pos (Markup.local_fact name);
-                map (Thm.transfer thy) (Facts.select thmref ths))
+                (Context_Position.report ctxt pos
+                  (Name_Space.markup_entry (Facts.space_of local_facts) name);
+                 map (Thm.transfer thy) (Facts.select thmref ths))
             | NONE => Global_Theory.get_fact (Context.Proof ctxt) thy xthmref);
       in pick name thms end;
 
diff -r c113db12bf8b -r d9fe47d21b41 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Apr 17 20:25:10 2011 +0200
+++ b/src/Pure/global_theory.ML	Sun Apr 17 20:58:43 2011 +0200
@@ -78,17 +78,21 @@
 
 fun get_fact context thy xthmref =
   let
+    val ctxt = Context.proof_of context;
+
+    val facts = facts_of thy;
     val xname = Facts.name_of_ref xthmref;
     val pos = Facts.pos_of_ref xthmref;
 
     val name = intern_fact thy xname;
-    val res = Facts.lookup context (facts_of thy) name;
+    val res = Facts.lookup context facts name;
     val _ = Theory.check_thy thy;
   in
     (case res of
       NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
     | SOME (static, ths) =>
-        (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name);
+        (Context_Position.report ctxt pos (Name_Space.markup_entry (Facts.space_of facts) name);
+         if static then () else Context_Position.report ctxt pos (Markup.dynamic_fact name);
          Facts.select xthmref (map (Thm.transfer thy) ths)))
   end;
 
diff -r c113db12bf8b -r d9fe47d21b41 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 20:25:10 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 20:58:43 2011 +0200
@@ -155,9 +155,7 @@
       Markup.FIXED_DECL -> FUNCTION,
       Markup.FIXED -> NULL,
       Markup.CONST -> LITERAL2,
-      Markup.FACT -> NULL,
       Markup.DYNAMIC_FACT -> LABEL,
-      Markup.LOCAL_FACT -> NULL,
       // inner syntax
       Markup.TFREE -> NULL,
       Markup.FREE -> MARKUP,