diff -r 30a67acd0d7e -r cc7a89d233f7 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Fri Aug 06 22:32:55 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Fri Aug 06 22:34:00 1999 +0200
@@ -9,7 +9,12 @@
 sig
   val write_keywords: unit -> unit
   val setup: (theory -> theory) list
+  val help: unit -> unit
+  val show_context: unit -> theory
+  val kill_goal: unit -> unit
+  val repeat_undo: int -> unit
   val init: bool -> unit
+  val isa_restart: unit -> unit
 end;
 
 structure ProofGeneral: PROOF_GENERAL =
@@ -91,12 +96,15 @@
 
 
 
-(** run-time initialization **)
+(** run-time operations **)
 
 (* messages *)
 
-fun decorate_lines bg en "" = std_output o suffix "\n" o enclose bg en
-  | decorate_lines bg en prfx = std_output o suffix "\n" o enclose bg en o prefix_lines prfx;
+val plain_output = std_output o suffix "\n";
+val plain_writeln = Library.setmp writeln_fn plain_output;
+
+fun decorate_lines bg en "" = plain_output o enclose bg en
+  | decorate_lines bg en prfx = plain_output o enclose bg en o prefix_lines prfx;
 
 fun setup_messages () =
  (writeln_fn := (decorate_lines (oct_char "360") (oct_char "361") "");
@@ -106,16 +114,19 @@
 
 (* theory / proof state *)
 
-fun setup_state () =
+fun print_current_goals n max th = plain_writeln (Goals.print_current_goals_default n max) th;
+
+fun setup_state isar =
   (current_goals_markers :=
     let
       val begin_state = oct_char "366";
       val end_state= oct_char "367";
       val begin_goal = oct_char "370";
     in (begin_state, end_state, begin_goal) end;
-  Toplevel.print_state_fn :=
-    (Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default);
-  Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
+  if isar then
+   (Toplevel.print_state_fn := plain_writeln Toplevel.print_state_default;
+    Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default))
+  else Goals.print_current_goals_fn := print_current_goals);
 
 
 (* theory loader actions *)
@@ -124,24 +135,50 @@
 
 fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
 
-fun trace_action ThyInfo.Update name = tell_pg "this theory is loaded:" name
-  | trace_action ThyInfo.Outdate name = tell_pg "you can unlock the theory" name
-  | trace_action ThyInfo.Remove name = tell_pg "you can unlock the theory" name;
+fun isa_action action name =
+  let val files = map (File.sysify_path o #1) (ThyInfo.loaded_files name) in
+    if action = ThyInfo.Update then seq (tell_pg "this file is loaded:") files
+    else seq (tell_pg "you can unlock the file") files
+  end;
+
+fun isar_action action name =
+  if action = ThyInfo.Update then tell_pg "this theory is loaded:" name
+  else tell_pg "you can unlock the theory" name;
 
 in
-  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
+  fun setup_thy_loader isar = ThyInfo.add_hook (if isar then isar_action else isa_action);
 end;
 
 
+(* some top-level commands for ProofGeneral/isa *)
+
+val help = writeln o Session.welcome;
+val show_context = Context.the_context;
+
+fun kill_goal () =
+  (Goal "PROP no_goal_supplied"; writeln ("Proof General, please clear the goals buffer."));
+
+fun repeat_undo 0 = ()
+  | repeat_undo n = (undo(); repeat_undo (n - 1));
+
+
+fun isa_restart () =
+ (ml_prompts (">" ^ oct_char "372") ("-" ^ oct_char "373");
+  ThyInfo.touch_all_thys ();
+  kill_goal ();
+  writeln ("Proof General, please clear the response buffer.");
+  writeln "Isabelle Proof General: Isabelle process ready!");
+
+
 (* init *)
 
 fun init isar =
  (setup_messages ();
-  setup_state ();
-  setup_thy_loader ();
+  setup_state isar;
+  setup_thy_loader isar;
   print_mode := [proof_generalN];
   set quick_and_dirty;
-  if isar then Isar.sync_main () else ());
+  if isar then Isar.sync_main () else isa_restart ());
 
 
 end;