added inform_file_processed, inform_file_retracted;
proper outer syntax setup;
more robust theory loader actions;

--- a/src/Pure/Interface/proof_general.ML	Tue Oct 26 19:05:26 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Tue Oct 26 19:06:52 1999 +0200
@@ -7,7 +7,6 @@
 
 signature PROOF_GENERAL =
 sig
-  val write_keywords: unit -> unit
   val setup: (theory -> theory) list
   val thms_containing: xstring list -> unit
   val help: unit -> unit
@@ -15,50 +14,15 @@
   val kill_goal: unit -> unit
   val repeat_undo: int -> unit
   val isa_restart: unit -> unit
+  val inform_file_processed: string -> unit
+  val inform_file_retracted: string -> unit
   val init: bool -> unit
+  val write_keywords: unit -> unit
 end;
 
 structure ProofGeneral: PROOF_GENERAL =
 struct
 
-
-(** generate keyword classification file **)
-
-local
-
-val regexp_meta = explode ".*+?[]^$";
-val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
-
-fun defconst name strs =
-  "\n(defconst isar-keywords-" ^ name ^
-  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
-
-fun make_elisp_commands commands kind =
-  defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
-
-fun make_elisp_syntax (keywords, commands) =
-  ";;\n\
-  \;; Keyword classification tables for Isabelle/Isar.\n\
-  \;; This file generated by Isabelle -- DO NOT EDIT!\n\
-  \;;\n\
-  \;; $" ^ "Id$\n\
-  \;;\n" ^
-  defconst "minor" (filter Syntax.is_identifier keywords) ^
-  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
-  "\n(provide 'isar-keywords)\n";
-
-val keywords_file = "isar-keywords.el";
-
-in
-
-fun write_keywords () =
-  File.write (Path.unpack keywords_file)
-    (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ()));
-
-end;
-
-
-
 (** compile-time theory setup **)
 
 (* token translations *)
@@ -119,7 +83,14 @@
   error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
 
 
-(* theory / proof state *)
+(* notification *)
+
+fun tell_clear_goals () = writeln "Proof General, please clear the goals buffer.";
+fun tell_clear_response () = writeln "Proof General, please clear the response buffer.";
+fun tell_file msg path = writeln ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
+
+
+(* theory / proof state output *)
 
 fun print_current_goals n max th = plain_writeln (Goals.print_current_goals_default n max) th;
 
@@ -141,39 +112,42 @@
 
 local
 
-fun tell_pg msg name = writeln ("Proof General, " ^ msg ^ " " ^ quote name);
+fun add_master_files name files =
+  let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
+  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
 
 fun trace_action action name =
-  let
-    val update = (action = ThyInfo.Update);
-    fun loaded (path, really) =
-      if update andalso not really then None
-      else Some path;
-    val tell = tell_pg (if update then "this file is loaded:" else "you can unlock the file")
-      o File.sysify_path;
-
-    val (master, files) = ThyInfo.loaded_files name;
-  in
-    (case master of
-      Some path => tell path
-    | None => tell (ThyLoad.thy_path name));     (*just to make sure ...*)
-    seq tell (mapfilter loaded files)
-  end;
+  if action = ThyInfo.Update then
+    seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
+  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
+    seq (tell_file "you can unlock the file") (add_master_files name (ThyInfo.loaded_files name))
+  else ();
 
 in
   fun setup_thy_loader () = ThyInfo.add_hook trace_action;
 end;
 
 
-(* some top-level commands for ProofGeneral/isa *)
+(* get informed about files *)
+
+val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
+
+(* FIXME improve, e.g. do something like pretend_use_thy *)
+fun inform_file_processed file =
+  ThyInfo.if_known_thy ThyInfo.touch_child_thys (thy_name file);
+
+fun inform_file_retracted file =
+  ThyInfo.if_known_thy ThyInfo.touch_child_thys (thy_name file);
+
+
+(* misc commands for ProofGeneral/isa *)
 
 fun thms_containing cs = ThmDatabase.print_thms_containing (the_context ()) cs;
 
 val help = writeln o Session.welcome;
 val show_context = Context.the_context;
 
-fun kill_goal () =
-  (Goals.reset_goals (); writeln "Proof General, please clear the goals buffer.");
+fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
 
 fun no_print_goals f = setmp print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
 
@@ -181,12 +155,49 @@
   | repeat_undo 1 = undo ()
   | repeat_undo n = (no_print_goals 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!");
+
+(* re-init process (an approximation) *)
+
+local
+
+fun restart isar =
+ (ThyInfo.touch_all_thys ();
+  if isar then () else (ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373"); kill_goal ());
+  tell_clear_response ();
+  writeln (Session.welcome ()));
+
+in
+
+fun isa_restart () = restart false;
+fun isar_restart () = (restart true; raise Toplevel.RESTART);
+
+end;
+
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterSyntax.Keyword in
+
+val restartP =
+  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
+    (P.opt_unit >> K (Toplevel.imperative isar_restart));
+
+val kill_proofP =
+  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
+    (Scan.succeed (IsarCmd.kill_proof_notify tell_clear_goals));
+
+val inform_file_processedP =
+  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
+    (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_processed name)));
+
+val inform_file_retractedP =
+  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
+    (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name)));
+
+fun init_outer_syntax () =
+  OuterSyntax.add_parsers [restartP, kill_proofP, inform_file_processedP, inform_file_retractedP];
+
+end;
 
 
 (* init *)
@@ -197,7 +208,46 @@
   setup_thy_loader ();
   print_mode := [proof_generalN];
   set quick_and_dirty;
+  if isar then init_outer_syntax () else ();
   if isar then Isar.sync_main () else isa_restart ());
 
 
+
+(** generate keyword classification file **)
+
+local
+
+val regexp_meta = explode ".*+?[]^$";
+val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
+
+fun defconst name strs =
+  "\n(defconst isar-keywords-" ^ name ^
+  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
+
+fun make_elisp_commands commands kind =
+  defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
+
+fun make_elisp_syntax (keywords, commands) =
+  ";;\n\
+  \;; Keyword classification tables for Isabelle/Isar.\n\
+  \;; This file generated by Isabelle -- DO NOT EDIT!\n\
+  \;;\n\
+  \;; $" ^ "Id$\n\
+  \;;\n" ^
+  defconst "minor" (filter Syntax.is_identifier keywords) ^
+  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
+  "\n(provide 'isar-keywords)\n";
+
+val keywords_file = "isar-keywords.el";
+
+in
+
+fun write_keywords () =
+  (init_outer_syntax ();
+    File.write (Path.unpack keywords_file)
+      (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
+
 end;
+
+
+end;