src/Pure/Isar/named_target.ML
author haftmann
Mon, 02 Jun 2014 19:21:41 +0200
changeset 57161 6254c51cd210
parent 57160 cf00d3c9db43
child 57176 88739947cc73
permissions -rw-r--r--
formal treatment of dangling parameters for class abbrevs analogously to class consts
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 41585
diff changeset
     1
(*  Title:      Pure/Isar/named_target.ML
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
30437
910a7aeb8dec more precise treatment of qualified bindings;
wenzelm
parents: 30364
diff changeset
     3
    Author:     Florian Haftmann, TU Muenchen
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
     4
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47061
diff changeset
     5
Targets for theory, locale, class -- at the bottom the nested structure.
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
     6
*)
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
     7
38350
480b2de9927c renamed Theory_Target to the more appropriate Named_Target
haftmann
parents: 38349
diff changeset
     8
signature NAMED_TARGET =
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
     9
sig
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47061
diff changeset
    10
  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
52140
88a69da5d3fa tuned structure
haftmann
parents: 52103
diff changeset
    11
  val is_theory: local_theory -> bool
41585
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    12
  val init: (local_theory -> local_theory) -> string -> theory -> local_theory
38388
94d5624dd1f7 Named_Target.theory_init
haftmann
parents: 38381
diff changeset
    13
  val theory_init: theory -> local_theory
38391
ba1cc1815ce1 named target is optional; explicit Name_Target.reinit
haftmann
parents: 38389
diff changeset
    14
  val reinit: local_theory -> local_theory -> local_theory
45488
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 45390
diff changeset
    15
  val context_cmd: xstring * Position.T -> theory -> local_theory
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    16
end;
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    17
38350
480b2de9927c renamed Theory_Target to the more appropriate Named_Target
haftmann
parents: 38349
diff changeset
    18
structure Named_Target: NAMED_TARGET =
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    19
struct
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
    20
21006
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    21
(* context data *)
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    22
41585
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    23
datatype target =
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    24
  Target of {target: string, is_locale: bool, is_class: bool,
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    25
    before_exit: local_theory -> local_theory};
25012
448af76a1ba3 pass explicit target record -- more informative peek operation;
wenzelm
parents: 25002
diff changeset
    26
41585
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    27
fun make_target target is_locale is_class before_exit =
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    28
  Target {target = target, is_locale = is_locale, is_class = is_class,
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    29
    before_exit = before_exit};
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    30
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    31
fun named_target _ "" before_exit = make_target "" false false before_exit
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    32
  | named_target thy locale before_exit =
38378
haftmann
parents: 38350
diff changeset
    33
      if Locale.defined thy locale
41585
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    34
      then make_target locale true (Class.is_class thy locale) before_exit
38378
haftmann
parents: 38350
diff changeset
    35
      else error ("No such locale: " ^ quote locale);
25012
448af76a1ba3 pass explicit target record -- more informative peek operation;
wenzelm
parents: 25002
diff changeset
    36
33519
e31a85f92ce9 adapted Generic_Data, Proof_Data;
wenzelm
parents: 33466
diff changeset
    37
structure Data = Proof_Data
21006
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    38
(
38391
ba1cc1815ce1 named target is optional; explicit Name_Target.reinit
haftmann
parents: 38389
diff changeset
    39
  type T = target option;
ba1cc1815ce1 named target is optional; explicit Name_Target.reinit
haftmann
parents: 38389
diff changeset
    40
  fun init _ = NONE;
21006
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    41
);
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    42
41585
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    43
val peek =
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    44
  Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
    45
    {target = target, is_locale = is_locale, is_class = is_class});
21006
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    46
53088
wenzelm
parents: 52140
diff changeset
    47
fun is_theory lthy =
wenzelm
parents: 52140
diff changeset
    48
  Option.map #target (peek lthy) = SOME "" andalso Local_Theory.level lthy = 1;
52140
88a69da5d3fa tuned structure
haftmann
parents: 52103
diff changeset
    49
21006
ac2732072403 added peek;
wenzelm
parents: 20984
diff changeset
    50
38318
1fade69519ab different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents: 38314
diff changeset
    51
(* define *)
1fade69519ab different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents: 38314
diff changeset
    52
57074
9a631586e3e5 tuned names
haftmann
parents: 57073
diff changeset
    53
fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params =
47289
wenzelm
parents: 47288
diff changeset
    54
  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
57074
9a631586e3e5 tuned names
haftmann
parents: 57073
diff changeset
    55
  #-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs)
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47279
diff changeset
    56
    #> pair (lhs, def));
38318
1fade69519ab different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents: 38314
diff changeset
    57
57074
9a631586e3e5 tuned names
haftmann
parents: 57073
diff changeset
    58
fun class_foundation class (((b, U), mx), (b_def, rhs)) params =
47289
wenzelm
parents: 47288
diff changeset
    59
  Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params
57074
9a631586e3e5 tuned names
haftmann
parents: 57073
diff changeset
    60
  #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params
47282
57d486231c92 more general standard_declaration;
wenzelm
parents: 47279
diff changeset
    61
    #> pair (lhs, def));
38318
1fade69519ab different foundations for different targets; simplified syntax handling of abbreviations
haftmann
parents: 38314
diff changeset
    62
57066
78651e94746f tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents: 57065
diff changeset
    63
fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
78651e94746f tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents: 57065
diff changeset
    64
  if is_class then class_foundation target
78651e94746f tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents: 57065
diff changeset
    65
  else if is_locale then locale_foundation target
47284
0e65b6a016dc clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm
parents: 47283
diff changeset
    66
  else Generic_Target.theory_foundation;
38303
ad4b59e9d0f9 factored out foundation of `define` into separate function
haftmann
parents: 38302
diff changeset
    67
24939
wenzelm
parents: 24935
diff changeset
    68
38308
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
    69
(* notes *)
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
    70
39639
haftmann
parents: 39557
diff changeset
    71
fun target_notes (Target {target, is_locale, ...}) =
47250
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47247
diff changeset
    72
  if is_locale then Generic_Target.locale_notes target
6523a21076a8 clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
wenzelm
parents: 47247
diff changeset
    73
  else Generic_Target.theory_notes;
38308
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
    74
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
    75
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
    76
(* abbrev *)
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
    77
57118
4760ac85b3f0 tuned signature
haftmann
parents: 57116
diff changeset
    78
fun locale_abbrev locale prmode (b, mx) global_rhs params =
57160
cf00d3c9db43 explicit passing of params
haftmann
parents: 57118
diff changeset
    79
  Generic_Target.background_abbrev (b, global_rhs) (snd params)
57074
9a631586e3e5 tuned names
haftmann
parents: 57073
diff changeset
    80
  #-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs));
38308
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
    81
57118
4760ac85b3f0 tuned signature
haftmann
parents: 57116
diff changeset
    82
fun class_abbrev class prmode (b, mx) global_rhs params =
57160
cf00d3c9db43 explicit passing of params
haftmann
parents: 57118
diff changeset
    83
  Generic_Target.background_abbrev (b, global_rhs) (snd params)
57161
6254c51cd210 formal treatment of dangling parameters for class abbrevs analogously to class consts
haftmann
parents: 57160
diff changeset
    84
  #-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs params);
57066
78651e94746f tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents: 57065
diff changeset
    85
78651e94746f tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents: 57065
diff changeset
    86
fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) =
78651e94746f tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents: 57065
diff changeset
    87
  if is_class then class_abbrev target
78651e94746f tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents: 57065
diff changeset
    88
  else if is_locale then locale_abbrev target
78651e94746f tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
haftmann
parents: 57065
diff changeset
    89
  else Generic_Target.theory_abbrev;
38308
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
    90
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
    91
47246
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47081
diff changeset
    92
(* declaration *)
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47081
diff changeset
    93
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47081
diff changeset
    94
fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
47279
4bab649dedf0 clarified standard_declaration vs. theory_declaration;
wenzelm
parents: 47278
diff changeset
    95
  if target = "" then Generic_Target.theory_declaration decl lthy
47246
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47081
diff changeset
    96
  else
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47081
diff changeset
    97
    lthy
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47081
diff changeset
    98
    |> pervasive ? Generic_Target.background_declaration decl
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47081
diff changeset
    99
    |> Generic_Target.locale_declaration target syntax decl
57065
2869310dae2a compactified
haftmann
parents: 57057
diff changeset
   100
    |> Generic_Target.standard_declaration (fn (_, other) => other <> 0) decl;
47246
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47081
diff changeset
   101
2bbab021c0e6 clarified Named_Target.target_declaration: propagate through other levels as well;
wenzelm
parents: 47081
diff changeset
   102
56723
a8f71445c265 subscription as target-specific implementation device
haftmann
parents: 56056
diff changeset
   103
(* subscription *)
a8f71445c265 subscription as target-specific implementation device
haftmann
parents: 56056
diff changeset
   104
a8f71445c265 subscription as target-specific implementation device
haftmann
parents: 56056
diff changeset
   105
fun target_subscription (Target {target, ...}) =
a8f71445c265 subscription as target-specific implementation device
haftmann
parents: 56056
diff changeset
   106
  if target = ""
a8f71445c265 subscription as target-specific implementation device
haftmann
parents: 56056
diff changeset
   107
  then Generic_Target.theory_registration
a8f71445c265 subscription as target-specific implementation device
haftmann
parents: 56056
diff changeset
   108
  else Generic_Target.locale_dependency target
a8f71445c265 subscription as target-specific implementation device
haftmann
parents: 56056
diff changeset
   109
a8f71445c265 subscription as target-specific implementation device
haftmann
parents: 56056
diff changeset
   110
38308
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   111
(* pretty *)
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   112
39639
haftmann
parents: 39557
diff changeset
   113
fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
38308
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   114
  let
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   115
    val target_name =
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 53088
diff changeset
   116
      [Pretty.keyword1 (if is_class then "class" else "locale"), Pretty.brk 1,
52103
fb577a13abbd more markup;
wenzelm
parents: 48102
diff changeset
   117
        Locale.pretty_name ctxt target];
45353
wenzelm
parents: 45352
diff changeset
   118
    val fixes =
wenzelm
parents: 45352
diff changeset
   119
      map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
wenzelm
parents: 45352
diff changeset
   120
        (#1 (Proof_Context.inferred_fixes ctxt));
wenzelm
parents: 45352
diff changeset
   121
    val assumes =
wenzelm
parents: 45352
diff changeset
   122
      map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
wenzelm
parents: 45352
diff changeset
   123
        (Assumption.all_assms_of ctxt);
38308
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   124
    val elems =
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   125
      (if null fixes then [] else [Element.Fixes fixes]) @
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   126
      (if null assumes then [] else [Element.Assumes assumes]);
40782
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39639
diff changeset
   127
    val body_elems =
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39639
diff changeset
   128
      if not is_locale then []
39639
haftmann
parents: 39557
diff changeset
   129
      else if null elems then [Pretty.block target_name]
haftmann
parents: 39557
diff changeset
   130
      else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
40782
aa533c5e3f48 superficial tuning;
wenzelm
parents: 39639
diff changeset
   131
        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
38308
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   132
  in
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 53088
diff changeset
   133
    Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41959
diff changeset
   134
      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))] :: body_elems
38308
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   135
  end;
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   136
0e4649095739 try to uniformly follow define/note/abbrev/declaration order as close as possible
haftmann
parents: 38307
diff changeset
   137
38378
haftmann
parents: 38350
diff changeset
   138
(* init *)
25291
870455627720 misc cleanup of init functions;
wenzelm
parents: 25269
diff changeset
   139
41585
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
   140
fun init_context (Target {target, is_locale, is_class, ...}) =
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 41959
diff changeset
   141
  if not is_locale then Proof_Context.init_global
29576
669b560fc2b9 wrecked old locale package and related modules
haftmann
parents: 29393
diff changeset
   142
  else if not is_class then Locale.init target
38379
67d71449e85b more convenient split of class modules: class and class_declaration
haftmann
parents: 38378
diff changeset
   143
  else Class.init target;
25269
f9090ae5cec9 clarified theory target interface
haftmann
parents: 25240
diff changeset
   144
41585
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
   145
fun init before_exit target thy =
39639
haftmann
parents: 39557
diff changeset
   146
  let
41585
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
   147
    val ta = named_target thy target before_exit;
47061
355317493f34 clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
wenzelm
parents: 47000
diff changeset
   148
    val naming = Sign.naming_of thy
355317493f34 clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
wenzelm
parents: 47000
diff changeset
   149
      |> Name_Space.mandatory_path (Long_Name.base_name target);
39639
haftmann
parents: 39557
diff changeset
   150
  in
haftmann
parents: 39557
diff changeset
   151
    thy
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 55763
diff changeset
   152
    |> Sign.change_begin
39639
haftmann
parents: 39557
diff changeset
   153
    |> init_context ta
haftmann
parents: 39557
diff changeset
   154
    |> Data.put (SOME ta)
47061
355317493f34 clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
wenzelm
parents: 47000
diff changeset
   155
    |> Local_Theory.init naming
39639
haftmann
parents: 39557
diff changeset
   156
       {define = Generic_Target.define (target_foundation ta),
haftmann
parents: 39557
diff changeset
   157
        notes = Generic_Target.notes (target_notes ta),
haftmann
parents: 39557
diff changeset
   158
        abbrev = Generic_Target.abbrev (target_abbrev ta),
45291
57cd50f98fdc uniform Local_Theory.declaration with explicit params;
wenzelm
parents: 45290
diff changeset
   159
        declaration = target_declaration ta,
56723
a8f71445c265 subscription as target-specific implementation device
haftmann
parents: 56056
diff changeset
   160
        subscription = target_subscription ta,
39639
haftmann
parents: 39557
diff changeset
   161
        pretty = pretty ta,
56056
4d46d53566e6 more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
wenzelm
parents: 55763
diff changeset
   162
        exit = before_exit #> Local_Theory.target_of #> Sign.change_end_local}
39639
haftmann
parents: 39557
diff changeset
   163
  end;
38247
12d3a5f04a72 unravelled target initialization code
haftmann
parents: 37314
diff changeset
   164
41585
45d7da4e4ccf added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
wenzelm
parents: 40782
diff changeset
   165
val theory_init = init I "";
25269
f9090ae5cec9 clarified theory target interface
haftmann
parents: 25240
diff changeset
   166
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47061
diff changeset
   167
val reinit =
47069
451fc10a81f3 more explicit Toplevel.open_target/close_target;
wenzelm
parents: 47066
diff changeset
   168
  Local_Theory.assert_bottom true #> Data.get #> the #>
47066
8a6124d09ff5 basic support for nested contexts including bundles;
wenzelm
parents: 47061
diff changeset
   169
  (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
38391
ba1cc1815ce1 named target is optional; explicit Name_Target.reinit
haftmann
parents: 38389
diff changeset
   170
47274
feef9b0b6031 misc tuning and simplification;
wenzelm
parents: 47251
diff changeset
   171
fun context_cmd ("-", _) thy = theory_init thy
45488
6d71d9e52369 pass positions for named targets, for formal links in the document model;
wenzelm
parents: 45390
diff changeset
   172
  | context_cmd target thy = init I (Locale.check thy target) thy;
33282
c6364889fea5 misc tuning;
wenzelm
parents: 33173
diff changeset
   173
20894
784eefc906aa Common theory targets.
wenzelm
parents:
diff changeset
   174
end;