src/Pure/Interface/proof_general.ML
changeset 7100 4f777a0e1c8b
parent 7027 ca0fbe679bbb
child 7193 cc7a89d233f7
equal deleted inserted replaced
7099:8142ccd13963 7100:4f777a0e1c8b
   116   Toplevel.print_state_fn :=
   116   Toplevel.print_state_fn :=
   117     (Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default);
   117     (Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default);
   118   Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
   118   Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
   119 
   119 
   120 
   120 
       
   121 (* theory loader actions *)
       
   122 
       
   123 local
       
   124 
       
   125 fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
       
   126 
       
   127 fun trace_action ThyInfo.Update name = tell_pg "this theory is loaded:" name
       
   128   | trace_action ThyInfo.Outdate name = tell_pg "you can unlock the theory" name
       
   129   | trace_action ThyInfo.Remove name = tell_pg "you can unlock the theory" name;
       
   130 
       
   131 in
       
   132   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
       
   133 end;
       
   134 
       
   135 
   121 (* init *)
   136 (* init *)
   122 
   137 
   123 fun init isar =
   138 fun init isar =
   124  (setup_messages ();
   139  (setup_messages ();
   125   setup_state ();
   140   setup_state ();
       
   141   setup_thy_loader ();
   126   print_mode := [proof_generalN];
   142   print_mode := [proof_generalN];
   127   set quick_and_dirty;
   143   set quick_and_dirty;
   128   if isar then Isar.sync_main () else ());
   144   if isar then Isar.sync_main () else ());
   129 
   145 
   130 
   146