23 structure Named_Target: NAMED_TARGET = |
23 structure Named_Target: NAMED_TARGET = |
24 struct |
24 struct |
25 |
25 |
26 (* context data *) |
26 (* context data *) |
27 |
27 |
|
28 datatype target = Theory | Locale of string | Class of string; |
|
29 |
|
30 fun ident_of_target Theory = "" |
|
31 | ident_of_target (Locale locale) = locale |
|
32 | ident_of_target (Class class) = class; |
|
33 |
|
34 fun target_is_theory (SOME Theory) = true |
|
35 | target_is_theory _ = false; |
|
36 |
|
37 fun locale_of_target (SOME (Locale locale)) = SOME locale |
|
38 | locale_of_target (SOME (Class locale)) = SOME locale |
|
39 | locale_of_target _ = NONE; |
|
40 |
|
41 fun class_of_target (SOME (Class class)) = SOME class |
|
42 | class_of_target _ = NONE; |
|
43 |
28 structure Data = Proof_Data |
44 structure Data = Proof_Data |
29 ( |
45 ( |
30 type T = (string * bool) option; |
46 type T = target option; |
31 fun init _ = NONE; |
47 fun init _ = NONE; |
32 ); |
48 ); |
33 |
49 |
34 val get_bottom_data = Data.get; |
50 val get_bottom_target = Data.get; |
35 |
51 |
36 fun get_data lthy = |
52 fun get_target lthy = |
37 if Local_Theory.level lthy = 1 |
53 if Local_Theory.level lthy = 1 |
38 then get_bottom_data lthy |
54 then get_bottom_target lthy |
39 else NONE; |
55 else NONE; |
40 |
56 |
41 fun is_theory lthy = |
57 fun ident_of lthy = |
42 (case get_data lthy of |
58 case get_target lthy of |
43 SOME ("", _) => true |
59 NONE => error "Not in a named target" |
44 | _ => false); |
60 | SOME target => ident_of_target target; |
45 |
61 |
46 fun target_of lthy = |
62 val is_theory = target_is_theory o get_target; |
47 (case get_data lthy of |
|
48 NONE => error "Not in a named target" |
|
49 | SOME (target, _) => target); |
|
50 |
63 |
51 fun locale_name_of NONE = NONE |
64 val locale_of = locale_of_target o get_target; |
52 | locale_name_of (SOME ("", _)) = NONE |
|
53 | locale_name_of (SOME (locale, _)) = SOME locale; |
|
54 |
65 |
55 val locale_of = locale_name_of o get_data; |
66 val bottom_locale_of = locale_of_target o get_bottom_target; |
56 |
67 |
57 val bottom_locale_of = locale_name_of o get_bottom_data; |
68 val class_of = class_of_target o get_target; |
58 |
|
59 fun class_of lthy = |
|
60 (case get_data lthy of |
|
61 SOME (class, true) => SOME class |
|
62 | _ => NONE); |
|
63 |
69 |
64 |
70 |
65 (* operations *) |
71 (* operations *) |
66 |
72 |
67 fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = |
73 fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = |
72 fun class_foundation class (((b, U), mx), (b_def, rhs)) params = |
78 fun class_foundation class (((b, U), mx), (b_def, rhs)) params = |
73 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
79 Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params |
74 #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params |
80 #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params |
75 #> pair (lhs, def)); |
81 #> pair (lhs, def)); |
76 |
82 |
77 fun foundation ("", _) = Generic_Target.theory_target_foundation |
83 fun foundation Theory = Generic_Target.theory_target_foundation |
78 | foundation (locale, false) = locale_foundation locale |
84 | foundation (Locale locale) = locale_foundation locale |
79 | foundation (class, true) = class_foundation class; |
85 | foundation (Class class) = class_foundation class; |
80 |
86 |
81 fun notes ("", _) = Generic_Target.theory_target_notes |
87 fun notes Theory = Generic_Target.theory_target_notes |
82 | notes (locale, _) = Generic_Target.locale_target_notes locale; |
88 | notes (Locale locale) = Generic_Target.locale_target_notes locale |
|
89 | notes (Class class) = Generic_Target.locale_target_notes class; |
83 |
90 |
84 fun abbrev ("", _) = Generic_Target.theory_abbrev |
91 fun abbrev Theory = Generic_Target.theory_abbrev |
85 | abbrev (locale, false) = Generic_Target.locale_abbrev locale |
92 | abbrev (Locale locale) = Generic_Target.locale_abbrev locale |
86 | abbrev (class, true) = Class.abbrev class; |
93 | abbrev (Class class) = Class.abbrev class; |
87 |
94 |
88 fun declaration ("", _) _ decl = Generic_Target.theory_declaration decl |
95 fun declaration Theory _ decl = Generic_Target.theory_declaration decl |
89 | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl; |
96 | declaration (Locale locale) flags decl = Generic_Target.locale_declaration locale flags decl |
|
97 | declaration (Class class) flags decl = Generic_Target.locale_declaration class flags decl; |
90 |
98 |
91 fun theory_registration ("", _) = Generic_Target.theory_registration |
99 fun theory_registration Theory = Generic_Target.theory_registration |
92 | theory_registration _ = (fn _ => error "Not possible in theory target"); |
100 | theory_registration _ = (fn _ => error "Not possible in theory target"); |
93 |
101 |
94 fun locale_dependency ("", false) = (fn _ => error "Not possible in locale target") |
102 fun locale_dependency Theory = (fn _ => error "Not possible in theory target") |
95 | locale_dependency ("", true) = (fn _ => error "Not possible in class target") |
103 | locale_dependency (Locale locale) = Generic_Target.locale_dependency locale |
96 | locale_dependency (locale, _) = Generic_Target.locale_dependency locale; |
104 | locale_dependency (Class class) = Generic_Target.locale_dependency class; |
97 |
105 |
98 fun pretty (target, is_class) ctxt = |
106 fun pretty Theory ctxt = |
99 if target = "" then |
107 [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, |
100 [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1, |
108 Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]] |
101 Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]] |
109 | pretty (Locale locale) ctxt = Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale |
102 else if is_class then Class.pretty_specification (Proof_Context.theory_of ctxt) target |
110 | pretty (Class class) ctxt = |
103 else |
111 Class.pretty_specification (Proof_Context.theory_of ctxt) class; |
104 (* FIXME pretty locale content *) |
|
105 let |
|
106 val target_name = [Pretty.keyword1 "locale", Pretty.brk 1, Locale.pretty_name ctxt target]; |
|
107 val fixes = |
|
108 map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) |
|
109 (#1 (Proof_Context.inferred_fixes ctxt)); |
|
110 val assumes = |
|
111 map (fn A => (Binding.empty_atts, [(Thm.term_of A, [])])) |
|
112 (Assumption.all_assms_of ctxt); |
|
113 val elems = |
|
114 (if null fixes then [] else [Element.Fixes fixes]) @ |
|
115 (if null assumes then [] else [Element.Assumes assumes]); |
|
116 in |
|
117 if null elems then [Pretty.block target_name] |
|
118 else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) :: |
|
119 map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))] |
|
120 end; |
|
121 |
112 |
122 |
113 |
123 (* init *) |
114 (* init *) |
124 |
115 |
125 fun make_name_data _ "" = ("", false) |
116 fun make_target _ "" = Theory |
126 | make_name_data thy target = |
117 | make_target thy ident = |
127 if Locale.defined thy target |
118 if Locale.defined thy ident |
128 then (target, Class.is_class thy target) |
119 then (if Class.is_class thy ident then Class else Locale) ident |
129 else error ("No such locale: " ^ quote target); |
120 else error ("No such locale: " ^ quote ident); |
130 |
121 |
131 fun init_context ("", _) = Proof_Context.init_global |
122 fun init_context Theory = Proof_Context.init_global |
132 | init_context (locale, false) = Locale.init locale |
123 | init_context (Locale locale) = Locale.init locale |
133 | init_context (class, true) = Class.init class; |
124 | init_context (Class class) = Class.init class; |
134 |
125 |
135 fun init before_exit target thy = |
126 fun init before_exit ident thy = |
136 let |
127 let |
137 val name_data = make_name_data thy target; |
128 val target = make_target thy ident; |
138 val background_naming = |
129 val background_naming = |
139 Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target); |
130 Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident); |
140 in |
131 in |
141 thy |
132 thy |
142 |> Sign.change_begin |
133 |> Sign.change_begin |
143 |> init_context name_data |
134 |> init_context target |
144 |> is_none before_exit ? Data.put (SOME name_data) |
135 |> is_none before_exit ? Data.put (SOME target) |
145 |> Local_Theory.init background_naming |
136 |> Local_Theory.init background_naming |
146 {define = Generic_Target.define (foundation name_data), |
137 {define = Generic_Target.define (foundation target), |
147 notes = Generic_Target.notes (notes name_data), |
138 notes = Generic_Target.notes (notes target), |
148 abbrev = abbrev name_data, |
139 abbrev = abbrev target, |
149 declaration = declaration name_data, |
140 declaration = declaration target, |
150 theory_registration = theory_registration name_data, |
141 theory_registration = theory_registration target, |
151 locale_dependency = locale_dependency name_data, |
142 locale_dependency = locale_dependency target, |
152 pretty = pretty name_data, |
143 pretty = pretty target, |
153 exit = the_default I before_exit |
144 exit = the_default I before_exit |
154 #> Local_Theory.target_of #> Sign.change_end_local} |
145 #> Local_Theory.target_of #> Sign.change_end_local} |
155 end; |
146 end; |
156 |
147 |
157 val theory_init = init NONE ""; |
148 val theory_init = init NONE ""; |
|
149 |
158 fun theory_map f = theory_init #> f #> Local_Theory.exit_global; |
150 fun theory_map f = theory_init #> f #> Local_Theory.exit_global; |
159 |
151 |
160 |
152 |
161 (* toplevel interaction *) |
153 (* toplevel interaction *) |
162 |
154 |