src/Pure/Interface/proof_general.ML
changeset 7100 4f777a0e1c8b
parent 7027 ca0fbe679bbb
child 7193 cc7a89d233f7
     1.1 --- a/src/Pure/Interface/proof_general.ML	Tue Jul 27 21:55:19 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Tue Jul 27 21:55:39 1999 +0200
     1.3 @@ -118,11 +118,27 @@
     1.4    Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
     1.5  
     1.6  
     1.7 +(* theory loader actions *)
     1.8 +
     1.9 +local
    1.10 +
    1.11 +fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
    1.12 +
    1.13 +fun trace_action ThyInfo.Update name = tell_pg "this theory is loaded:" name
    1.14 +  | trace_action ThyInfo.Outdate name = tell_pg "you can unlock the theory" name
    1.15 +  | trace_action ThyInfo.Remove name = tell_pg "you can unlock the theory" name;
    1.16 +
    1.17 +in
    1.18 +  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
    1.19 +end;
    1.20 +
    1.21 +
    1.22  (* init *)
    1.23  
    1.24  fun init isar =
    1.25   (setup_messages ();
    1.26    setup_state ();
    1.27 +  setup_thy_loader ();
    1.28    print_mode := [proof_generalN];
    1.29    set quick_and_dirty;
    1.30    if isar then Isar.sync_main () else ());