# HG changeset patch # User wenzelm # Date 1427210227 -3600 # Node ID 45c89526208f0c6cb4ed3cdb162a7d30ab199da1 # Parent f313ca9fbba0ab7947b0499d7bf27070ce8deaec tuned; diff -r f313ca9fbba0 -r 45c89526208f src/Pure/variable.ML --- a/src/Pure/variable.ML Tue Mar 24 16:16:48 2015 +0100 +++ b/src/Pure/variable.ML Tue Mar 24 16:17:07 2015 +0100 @@ -6,9 +6,6 @@ signature VARIABLE = sig - val is_body: Proof.context -> bool - val set_body: bool -> Proof.context -> Proof.context - val restore_body: Proof.context -> Proof.context -> Proof.context val names_of: Proof.context -> Name.context val binds_of: Proof.context -> (typ * term) Vartab.table val maxidx_of: Proof.context -> int @@ -34,6 +31,9 @@ val declare_const: string * string -> Proof.context -> Proof.context val next_bound: string * typ -> Proof.context -> term * Proof.context val revert_bounds: Proof.context -> term -> term + val is_body: Proof.context -> bool + val set_body: bool -> Proof.context -> Proof.context + val restore_body: Proof.context -> Proof.context -> Proof.context val improper_fixes: Proof.context -> Proof.context val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context val is_improper: Proof.context -> string -> bool @@ -90,8 +90,7 @@ val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN; datatype data = Data of - {is_body: bool, (*inner body mode*) - names: Name.context, (*type/term variable names*) + {names: Name.context, (*type/term variable names*) consts: string Symtab.table, (*consts within the local scope*) bounds: int * ((string * typ) * string) list, (*next index, internal name, type, external name*) fixes: fixes, (*term fixes -- global name space, intern ~> extern*) @@ -103,13 +102,12 @@ typ Vartab.table * (*type constraints*) sort Vartab.table}; (*default sorts*) -fun make_data - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) = - Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes, - binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; +fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) = + Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds, + type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; val empty_data = - make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, + make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); structure Data = Proof_Data @@ -119,66 +117,47 @@ ); fun map_data f = - Data.map (fn - Data {is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} => - make_data - (f (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints))); + Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} => + make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints))); fun map_names f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (f names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); fun map_consts f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, f consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); fun map_bounds f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, f bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); fun map_fixes f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, f fixes, binds, type_occs, maxidx, sorts, constraints)); fun map_binds f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, f binds, type_occs, maxidx, sorts, constraints)); fun map_type_occs f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, binds, f type_occs, maxidx, sorts, constraints)); fun map_maxidx f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, binds, type_occs, f maxidx, sorts, constraints)); fun map_sorts f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, binds, type_occs, maxidx, f sorts, constraints)); fun map_constraints f = - map_data (fn - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints)); + map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => + (names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, f constraints)); fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); -val is_body = #is_body o rep_data; - -fun set_body b = - map_data (fn (_, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) => - (b, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints)); - -fun restore_body ctxt = set_body (is_body ctxt); - val names_of = #names o rep_data; val fixes_of = #fixes o rep_data; val fixes_space = Name_Space.space_of_table o fixes_of; @@ -339,6 +318,16 @@ (** fixes **) +(* inner body mode *) + +val inner_body = + Config.bool (Config.declare ("inner_body", @{here}) (K (Config.Bool false))); + +fun is_body ctxt = Config.get ctxt inner_body; +val set_body = Config.put inner_body; +fun restore_body ctxt = set_body (is_body ctxt); + + (* proper mode *) val proper_fixes =