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