equal
deleted
inserted
replaced
71 end; |
71 end; |
72 |
72 |
73 val type_syntax = target_decl Locale.add_type_syntax; |
73 val type_syntax = target_decl Locale.add_type_syntax; |
74 val term_syntax = target_decl Locale.add_term_syntax; |
74 val term_syntax = target_decl Locale.add_term_syntax; |
75 val declaration = target_decl Locale.add_declaration; |
75 val declaration = target_decl Locale.add_declaration; |
76 |
|
77 fun target_naming (Target {target, ...}) lthy = |
|
78 (if target = "" then Sign.naming_of (ProofContext.theory_of lthy) |
|
79 else ProofContext.naming_of (LocalTheory.target_of lthy)) |
|
80 |> NameSpace.qualified_names; |
|
81 |
76 |
82 fun class_target (Target {target, ...}) f = |
77 fun class_target (Target {target, ...}) f = |
83 LocalTheory.raw_theory f #> |
78 LocalTheory.raw_theory f #> |
84 LocalTheory.target (Class.refresh_syntax target); |
79 LocalTheory.target (Class.refresh_syntax target); |
85 |
80 |
319 define = define ta, |
314 define = define ta, |
320 notes = notes ta, |
315 notes = notes ta, |
321 type_syntax = type_syntax ta, |
316 type_syntax = type_syntax ta, |
322 term_syntax = term_syntax ta, |
317 term_syntax = term_syntax ta, |
323 declaration = declaration ta, |
318 declaration = declaration ta, |
324 target_naming = target_naming ta, |
|
325 reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy), |
319 reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy), |
326 exit = LocalTheory.target_of} |
320 exit = LocalTheory.target_of} |
327 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta; |
321 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta; |
328 |
322 |
329 in |
323 in |