61 case get_data lthy of |
61 case get_data lthy of |
62 SOME (class, true) => SOME class |
62 SOME (class, true) => SOME class |
63 | _ => NONE; |
63 | _ => NONE; |
64 |
64 |
65 |
65 |
66 (* define *) |
66 (* operations *) |
67 |
67 |
68 fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = |
68 fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = |
69 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
69 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
70 #-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) |
70 #-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) |
71 #> pair (lhs, def)); |
71 #> pair (lhs, def)); |
77 |
77 |
78 fun foundation ("", _) = Generic_Target.theory_target_foundation |
78 fun foundation ("", _) = Generic_Target.theory_target_foundation |
79 | foundation (locale, false) = locale_foundation locale |
79 | foundation (locale, false) = locale_foundation locale |
80 | foundation (class, true) = class_foundation class; |
80 | foundation (class, true) = class_foundation class; |
81 |
81 |
82 |
|
83 (* notes *) |
|
84 |
|
85 fun notes ("", _) = Generic_Target.theory_target_notes |
82 fun notes ("", _) = Generic_Target.theory_target_notes |
86 | notes (locale, _) = Generic_Target.locale_target_notes locale; |
83 | notes (locale, _) = Generic_Target.locale_target_notes locale; |
87 |
|
88 |
|
89 (* abbrev *) |
|
90 |
84 |
91 fun abbrev ("", _) = Generic_Target.theory_abbrev |
85 fun abbrev ("", _) = Generic_Target.theory_abbrev |
92 | abbrev (locale, false) = Generic_Target.locale_abbrev locale |
86 | abbrev (locale, false) = Generic_Target.locale_abbrev locale |
93 | abbrev (class, true) = Class.abbrev class; |
87 | abbrev (class, true) = Class.abbrev class; |
94 |
88 |
95 |
|
96 (* declaration *) |
|
97 |
|
98 fun declaration ("", _) flags decl = Generic_Target.theory_declaration decl |
89 fun declaration ("", _) flags decl = Generic_Target.theory_declaration decl |
99 | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl; |
90 | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl; |
100 |
91 |
101 |
|
102 (* subscription *) |
|
103 |
|
104 fun subscription ("", _) = Generic_Target.theory_registration |
92 fun subscription ("", _) = Generic_Target.theory_registration |
105 | subscription (locale, _) = Generic_Target.locale_dependency locale; |
93 | subscription (locale, _) = Generic_Target.locale_dependency locale; |
106 |
|
107 |
|
108 (* pretty *) |
|
109 |
94 |
110 fun pretty (target, is_class) ctxt = |
95 fun pretty (target, is_class) ctxt = |
111 if target = "" then |
96 if target = "" then |
112 [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, |
97 [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, |
113 Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]] |
98 Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]] |