renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
authorwenzelm
Mon May 10 20:53:06 2010 +0200 (2010-05-10)
changeset 36787f60e4dd6d76f
parent 36786 b7a62e7dec00
child 36788 1fd4f28e6ce1
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
src/HOL/Mirabelle/Tools/mirabelle.ML
src/Provers/blast.ML
src/Pure/Isar/attrib.ML
src/Pure/config.ML
src/Pure/unify.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon May 10 17:37:32 2010 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon May 10 20:53:06 2010 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4  
     1.5  fun log thy s =
     1.6    let fun append_to n = if n = "" then K () else File.append (Path.explode n)
     1.7 -  in append_to (Config.get_thy thy logfile) (s ^ "\n") end
     1.8 +  in append_to (Config.get_global thy logfile) (s ^ "\n") end
     1.9    (* FIXME: with multithreading and parallel proofs enabled, we might need to
    1.10       encapsulate this inside a critical section *)
    1.11  
    1.12 @@ -108,7 +108,7 @@
    1.13    | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
    1.14  
    1.15  fun only_within_range thy pos f x =
    1.16 -  let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
    1.17 +  let val l = Config.get_global thy start_line and r = Config.get_global thy end_line
    1.18    in if in_range l r (Position.line_of pos) then f x else () end
    1.19  
    1.20  in
    1.21 @@ -118,7 +118,7 @@
    1.22      val thy = Proof.theory_of pre
    1.23      val pos = Toplevel.pos_of tr
    1.24      val name = Toplevel.name_of tr
    1.25 -    val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
    1.26 +    val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout))
    1.27  
    1.28      val str0 = string_of_int o the_default 0
    1.29      val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
     2.1 --- a/src/Provers/blast.ML	Mon May 10 17:37:32 2010 +0200
     2.2 +++ b/src/Provers/blast.ML	Mon May 10 20:53:06 2010 +0200
     2.3 @@ -1278,7 +1278,7 @@
     2.4  val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
     2.5  
     2.6  fun blast_tac cs i st =
     2.7 -    ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
     2.8 +    ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
     2.9          (timing_depth_tac (start_timing ()) cs) 0) i
    2.10       THEN flexflex_tac) st
    2.11      handle TRANS s =>
     3.1 --- a/src/Pure/Isar/attrib.ML	Mon May 10 17:37:32 2010 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Mon May 10 20:53:06 2010 +0200
     3.3 @@ -355,7 +355,7 @@
     3.4    | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
     3.5  
     3.6  fun scan_config thy config =
     3.7 -  let val config_type = Config.get_thy thy config
     3.8 +  let val config_type = Config.get_global thy config
     3.9    in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
    3.10  
    3.11  in
     4.1 --- a/src/Pure/config.ML	Mon May 10 17:37:32 2010 +0200
     4.2 +++ b/src/Pure/config.ML	Mon May 10 20:53:06 2010 +0200
     4.3 @@ -16,9 +16,9 @@
     4.4    val get: Proof.context -> 'a T -> 'a
     4.5    val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
     4.6    val put: 'a T -> 'a -> Proof.context -> Proof.context
     4.7 -  val get_thy: theory -> 'a T -> 'a
     4.8 -  val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
     4.9 -  val put_thy: 'a T -> 'a -> theory -> theory
    4.10 +  val get_global: theory -> 'a T -> 'a
    4.11 +  val map_global: 'a T -> ('a -> 'a) -> theory -> theory
    4.12 +  val put_global: 'a T -> 'a -> theory -> theory
    4.13    val get_generic: Context.generic -> 'a T -> 'a
    4.14    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    4.15    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    4.16 @@ -83,9 +83,9 @@
    4.17  fun map_ctxt config f = Context.proof_map (map_generic config f);
    4.18  fun put_ctxt config value = map_ctxt config (K value);
    4.19  
    4.20 -fun get_thy thy = get_generic (Context.Theory thy);
    4.21 -fun map_thy config f = Context.theory_map (map_generic config f);
    4.22 -fun put_thy config value = map_thy config (K value);
    4.23 +fun get_global thy = get_generic (Context.Theory thy);
    4.24 +fun map_global config f = Context.theory_map (map_generic config f);
    4.25 +fun put_global config value = map_global config (K value);
    4.26  
    4.27  
    4.28  (* context information *)
     5.1 --- a/src/Pure/unify.ML	Mon May 10 17:37:32 2010 +0200
     5.2 +++ b/src/Pure/unify.ML	Mon May 10 20:53:06 2010 +0200
     5.3 @@ -349,7 +349,7 @@
     5.4  fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
     5.5    : (term * (Envir.env * dpair list))Seq.seq =
     5.6  let
     5.7 -  val trace_tps = Config.get_thy thy trace_types;
     5.8 +  val trace_tps = Config.get_global thy trace_types;
     5.9    (*Produce copies of uarg and cons them in front of uargs*)
    5.10    fun copycons uarg (uargs, (env, dpairs)) =
    5.11    Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
    5.12 @@ -584,9 +584,9 @@
    5.13  fun hounifiers (thy,env, tus : (term*term)list)
    5.14    : (Envir.env * (term*term)list)Seq.seq =
    5.15    let
    5.16 -    val trace_bnd = Config.get_thy thy trace_bound;
    5.17 -    val search_bnd = Config.get_thy thy search_bound;
    5.18 -    val trace_smp = Config.get_thy thy trace_simp;
    5.19 +    val trace_bnd = Config.get_global thy trace_bound;
    5.20 +    val search_bnd = Config.get_global thy search_bound;
    5.21 +    val trace_smp = Config.get_global thy trace_simp;
    5.22      fun add_unify tdepth ((env,dpairs), reseq) =
    5.23      Seq.make (fn()=>
    5.24      let val (env',flexflex,flexrigid) =