tuned;
authorwenzelm
Thu May 12 10:03:17 2016 +0200 (2016-05-12 ago)
changeset 63083c672c34ab042
parent 63081 5a5beb3dbe7e
child 63084 0054992a86b7
tuned;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed May 11 16:13:17 2016 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu May 12 10:03:17 2016 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4    val get_global: theory -> string -> Proof.context
     1.5    type mode
     1.6    val mode_default: mode
     1.7 -  val mode_stmt: mode
     1.8    val mode_pattern: mode
     1.9    val mode_schematic: mode
    1.10    val mode_abbrev: mode
    1.11 @@ -21,7 +20,6 @@
    1.12    val get_mode: Proof.context -> mode
    1.13    val restore_mode: Proof.context -> Proof.context -> Proof.context
    1.14    val abbrev_mode: Proof.context -> bool
    1.15 -  val set_stmt: bool -> Proof.context -> Proof.context
    1.16    val syn_of: Proof.context -> Syntax.syntax
    1.17    val tsig_of: Proof.context -> Type.tsig
    1.18    val set_defsort: sort -> Proof.context -> Proof.context
    1.19 @@ -125,6 +123,8 @@
    1.20    val get_fact_single: Proof.context -> Facts.ref -> thm
    1.21    val get_thms: Proof.context -> xstring -> thm list
    1.22    val get_thm: Proof.context -> xstring -> thm
    1.23 +  val set_stmt: bool -> Proof.context -> Proof.context
    1.24 +  val restore_stmt: Proof.context -> Proof.context -> Proof.context
    1.25    val add_thms_dynamic: binding * (Context.generic -> thm list) ->
    1.26      Proof.context -> string * Proof.context
    1.27    val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
    1.28 @@ -207,20 +207,17 @@
    1.29  
    1.30  datatype mode =
    1.31    Mode of
    1.32 -   {stmt: bool,                (*inner statement mode*)
    1.33 -    pattern: bool,             (*pattern binding schematic variables*)
    1.34 +   {pattern: bool,             (*pattern binding schematic variables*)
    1.35      schematic: bool,           (*term referencing loose schematic variables*)
    1.36      abbrev: bool};             (*abbrev mode -- no normalization*)
    1.37  
    1.38 -fun make_mode (stmt, pattern, schematic, abbrev) =
    1.39 -  Mode {stmt = stmt, pattern = pattern, schematic = schematic, abbrev = abbrev};
    1.40 +fun make_mode (pattern, schematic, abbrev) =
    1.41 +  Mode {pattern = pattern, schematic = schematic, abbrev = abbrev};
    1.42  
    1.43 -val mode_default   = make_mode (false, false, false, false);
    1.44 -val mode_stmt      = make_mode (true, false, false, false);
    1.45 -val mode_pattern   = make_mode (false, true, false, false);
    1.46 -val mode_schematic = make_mode (false, false, true, false);
    1.47 -val mode_abbrev    = make_mode (false, false, false, true);
    1.48 -
    1.49 +val mode_default   = make_mode (false, false, false);
    1.50 +val mode_pattern   = make_mode (true, false, false);
    1.51 +val mode_schematic = make_mode (false, true, false);
    1.52 +val mode_abbrev    = make_mode (false, false, true);
    1.53  
    1.54  
    1.55  (** Isar proof context information **)
    1.56 @@ -266,8 +263,8 @@
    1.57    (mode, syntax, tsig, consts, facts, cases));
    1.58  
    1.59  fun map_mode f =
    1.60 -  map_data (fn (Mode {stmt, pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) =>
    1.61 -    (make_mode (f (stmt, pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases));
    1.62 +  map_data (fn (Mode {pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) =>
    1.63 +    (make_mode (f (pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases));
    1.64  
    1.65  fun map_syntax f =
    1.66    map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
    1.67 @@ -303,9 +300,6 @@
    1.68  val restore_mode = set_mode o get_mode;
    1.69  val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
    1.70  
    1.71 -fun set_stmt stmt =
    1.72 -  map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
    1.73 -
    1.74  val syntax_of = #syntax o rep_data;
    1.75  val syn_of = Local_Syntax.syn_of o syntax_of;
    1.76  val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
    1.77 @@ -1041,6 +1035,16 @@
    1.78  end;
    1.79  
    1.80  
    1.81 +(* inner statement mode *)
    1.82 +
    1.83 +val inner_stmt =
    1.84 +  Config.bool (Config.declare ("inner_stmt", @{here}) (K (Config.Bool false)));
    1.85 +
    1.86 +fun is_stmt ctxt = Config.get ctxt inner_stmt;
    1.87 +val set_stmt = Config.put inner_stmt;
    1.88 +val restore_stmt = set_stmt o is_stmt;
    1.89 +
    1.90 +
    1.91  (* facts *)
    1.92  
    1.93  fun add_thms_dynamic arg ctxt =
    1.94 @@ -1062,8 +1066,8 @@
    1.95        fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths;
    1.96      val (res, ctxt') = fold_map app facts ctxt;
    1.97      val thms = Global_Theory.name_thms false false name (flat res);
    1.98 -    val Mode {stmt, ...} = get_mode ctxt;
    1.99 -  in ((name, thms), ctxt' |> update_thms {strict = false, index = stmt} (b, SOME thms)) end);
   1.100 +    val index = is_stmt ctxt;
   1.101 +  in ((name, thms), ctxt' |> update_thms {strict = false, index = index} (b, SOME thms)) end);
   1.102  
   1.103  fun put_thms index thms ctxt = ctxt
   1.104    |> map_naming (K Name_Space.local_naming)