eliminated obsolete markup -- superseded by generic "entity" markup;
authorwenzelm
Sun Apr 17 20:15:46 2011 +0200 (2011-04-17)
changeset 42376c3abf2c3f541
parent 42375 774df7c59508
child 42377 c113db12bf8b
eliminated obsolete markup -- superseded by generic "entity" markup;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/Isar/proof_context.ML
src/Pure/global_theory.ML
src/Pure/sign.ML
src/Tools/jEdit/src/jedit/isabelle_markup.scala
     1.1 --- a/src/Pure/General/markup.ML	Sun Apr 17 19:54:04 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Sun Apr 17 20:15:46 2011 +0200
     1.3 @@ -38,12 +38,9 @@
     1.4    val tyconN: string val tycon: string -> T
     1.5    val fixed_declN: string val fixed_decl: string -> T
     1.6    val fixedN: string val fixed: string -> T
     1.7 -  val const_declN: string val const_decl: string -> T
     1.8    val constN: string val const: string -> T
     1.9 -  val fact_declN: string val fact_decl: string -> T
    1.10    val factN: string val fact: string -> T
    1.11    val dynamic_factN: string val dynamic_fact: string -> T
    1.12 -  val local_fact_declN: string val local_fact_decl: string -> T
    1.13    val local_factN: string val local_fact: string -> T
    1.14    val tfreeN: string val tfree: T
    1.15    val tvarN: string val tvar: T
    1.16 @@ -218,12 +215,9 @@
    1.17  val (tyconN, tycon) = markup_string "tycon" nameN;
    1.18  val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
    1.19  val (fixedN, fixed) = markup_string "fixed" nameN;
    1.20 -val (const_declN, const_decl) = markup_string "const_decl" nameN;
    1.21  val (constN, const) = markup_string "constant" nameN;
    1.22 -val (fact_declN, fact_decl) = markup_string "fact_decl" nameN;
    1.23  val (factN, fact) = markup_string "fact" nameN;
    1.24  val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
    1.25 -val (local_fact_declN, local_fact_decl) = markup_string "local_fact_decl" nameN;
    1.26  val (local_factN, local_fact) = markup_string "local_fact" nameN;
    1.27  
    1.28  
     2.1 --- a/src/Pure/General/markup.scala	Sun Apr 17 19:54:04 2011 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Sun Apr 17 20:15:46 2011 +0200
     2.3 @@ -151,12 +151,9 @@
     2.4    val TYCON = "tycon"
     2.5    val FIXED_DECL = "fixed_decl"
     2.6    val FIXED = "fixed"
     2.7 -  val CONST_DECL = "const_decl"
     2.8    val CONST = "constant"
     2.9 -  val FACT_DECL = "fact_decl"
    2.10    val FACT = "fact"
    2.11    val DYNAMIC_FACT = "dynamic_fact"
    2.12 -  val LOCAL_FACT_DECL = "local_fact_decl"
    2.13    val LOCAL_FACT = "local_fact"
    2.14  
    2.15  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 19:54:04 2011 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Apr 17 20:15:46 2011 +0200
     3.3 @@ -912,10 +912,7 @@
     3.4  
     3.5  fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
     3.6    let
     3.7 -    val pos = Binding.pos_of b;
     3.8      val name = full_name ctxt b;
     3.9 -    val _ = Context_Position.report ctxt pos (Markup.local_fact_decl name);
    3.10 -
    3.11      val facts = Global_Theory.name_thmss false name raw_facts;
    3.12      fun app (th, attrs) x =
    3.13        swap (Library.foldl_map
     4.1 --- a/src/Pure/global_theory.ML	Sun Apr 17 19:54:04 2011 +0200
     4.2 +++ b/src/Pure/global_theory.ML	Sun Apr 17 20:15:46 2011 +0200
     4.3 @@ -185,10 +185,7 @@
     4.4  
     4.5  fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
     4.6    let
     4.7 -    val pos = Binding.pos_of b;
     4.8      val name = Sign.full_name thy b;
     4.9 -    val _ = Position.report pos (Markup.fact_decl name);
    4.10 -
    4.11      fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
    4.12      val (thms, thy') = thy |> enter_thms
    4.13        (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app)
     5.1 --- a/src/Pure/sign.ML	Sun Apr 17 19:54:04 2011 +0200
     5.2 +++ b/src/Pure/sign.ML	Sun Apr 17 20:15:46 2011 +0200
     5.3 @@ -419,13 +419,7 @@
     5.4  fun add_consts_i args thy =
     5.5    #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
     5.6  
     5.7 -fun declare_const ctxt ((b, T), mx) thy =
     5.8 -  let
     5.9 -    val pos = Binding.pos_of b;
    5.10 -    val ([const as Const (c, _)], thy') = gen_add_consts (K I) ctxt [(b, T, mx)] thy;
    5.11 -    val _ = Position.report pos (Markup.const_decl c);
    5.12 -  in (const, thy') end;
    5.13 -
    5.14 +fun declare_const ctxt ((b, T), mx) = yield_singleton (gen_add_consts (K I) ctxt) (b, T, mx);
    5.15  fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy;
    5.16  
    5.17  end;
     6.1 --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 19:54:04 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 20:15:46 2011 +0200
     6.3 @@ -154,12 +154,9 @@
     6.4        Markup.TYCON -> NULL,
     6.5        Markup.FIXED_DECL -> FUNCTION,
     6.6        Markup.FIXED -> NULL,
     6.7 -      Markup.CONST_DECL -> FUNCTION,
     6.8        Markup.CONST -> LITERAL2,
     6.9 -      Markup.FACT_DECL -> FUNCTION,
    6.10        Markup.FACT -> NULL,
    6.11        Markup.DYNAMIC_FACT -> LABEL,
    6.12 -      Markup.LOCAL_FACT_DECL -> FUNCTION,
    6.13        Markup.LOCAL_FACT -> NULL,
    6.14        // inner syntax
    6.15        Markup.TFREE -> NULL,