equal
deleted
inserted
replaced
141 |
141 |
142 local |
142 local |
143 |
143 |
144 fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name); |
144 fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name); |
145 |
145 |
146 fun isa_action action name = |
146 fun trace_action action name = |
147 let |
147 let |
148 val update = (action = ThyInfo.Update); |
148 val update = (action = ThyInfo.Update); |
149 fun loaded ((path, _), really) = |
149 fun loaded ((path, _), really) = |
150 if update andalso not really then None |
150 if update andalso not really then None |
151 else Some (File.sysify_path path); |
151 else Some (File.sysify_path path); |
153 in |
153 in |
154 if update then seq (tell_pg "this file is loaded:") files |
154 if update then seq (tell_pg "this file is loaded:") files |
155 else seq (tell_pg "you can unlock the file") files |
155 else seq (tell_pg "you can unlock the file") files |
156 end; |
156 end; |
157 |
157 |
158 fun isar_action action name = |
|
159 if action = ThyInfo.Update then tell_pg "this theory is loaded:" name |
|
160 else tell_pg "you can unlock the theory" name; |
|
161 |
|
162 in |
158 in |
163 fun setup_thy_loader isar = ThyInfo.add_hook (if isar then isar_action else isa_action); |
159 fun setup_thy_loader () = ThyInfo.add_hook trace_action; |
164 end; |
160 end; |
165 |
161 |
166 |
162 |
167 (* some top-level commands for ProofGeneral/isa *) |
163 (* some top-level commands for ProofGeneral/isa *) |
168 |
164 |
188 (* init *) |
184 (* init *) |
189 |
185 |
190 fun init isar = |
186 fun init isar = |
191 (setup_messages (); |
187 (setup_messages (); |
192 setup_state isar; |
188 setup_state isar; |
193 setup_thy_loader isar; |
189 setup_thy_loader (); |
194 print_mode := [proof_generalN]; |
190 print_mode := [proof_generalN]; |
195 set quick_and_dirty; |
191 set quick_and_dirty; |
196 if isar then Isar.sync_main () else isa_restart ()); |
192 if isar then Isar.sync_main () else isa_restart ()); |
197 |
193 |
198 |
194 |