tuned signature;

--- a/src/Pure/ProofGeneral/preferences.ML	Mon May 13 21:42:27 2013 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Mon May 13 22:00:19 2013 +0200
@@ -26,6 +26,7 @@
   val nat_pref: int Unsynchronized.ref -> string -> string -> preference
   val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
   type T = (string * preference list) list
+  val thm_depsN: string
   val pure_preferences: T
   val remove: string -> T -> T
   val add: string -> preference -> T -> T

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon May 13 21:42:27 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon May 13 22:00:19 2013 +0200
@@ -140,9 +140,34 @@
   welcome ());
 
 
-(* theorem dependency output *)
+(* theorem dependencies *)
+
+local
+
+fun add_proof_body (PBody {thms, ...}) =
+  thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
 
-val thm_depsN = "thm_deps";
+fun add_thm th =
+  (case Thm.proof_body_of th of
+    PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
+      if Thm.has_name_hint th andalso Thm.get_name_hint th = name
+      then add_proof_body (Future.join body)
+      else I
+  | body => add_proof_body body);
+
+in
+
+fun thm_deps ths =
+  let
+    (* FIXME proper derivation names!? *)
+    val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
+    val deps = Symtab.keys (fold add_thm ths Symtab.empty);
+  in (names, deps) end;
+
+end;
+
+
+(* report theorem dependencies *)
 
 local
 
@@ -154,11 +179,13 @@
 in
 
 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
-  if print_mode_active thm_depsN andalso
+  if print_mode_active Preferences.thm_depsN andalso
     can Toplevel.theory_of state andalso Toplevel.is_theory state'
   then
-    let val (names, deps) =
-      ProofGeneralPgip.new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state')
+    let
+      val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state);
+      val facts = Global_Theory.facts_of (Toplevel.theory_of state');
+      val (names, deps) = thm_deps (maps #2 (Facts.dest_static [prev_facts] facts));
     in
       if null names orelse null deps then ()
       else thm_deps_message (spaces_quote names, spaces_quote deps)
@@ -205,21 +232,23 @@
 
 (* init *)
 
+val proof_general_emacsN = "ProofGeneralEmacs";
+
 val initialized = Unsynchronized.ref false;
 
 fun init () =
   (if ! initialized then ()
    else
     (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
-     Output.add_mode ProofGeneralPgip.proof_general_emacsN
+     Output.add_mode proof_general_emacsN
       Output.default_output Output.default_escape;
-     Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
+     Markup.add_mode proof_general_emacsN YXML.output_markup;
      setup_messages ();
      setup_thy_loader ();
      setup_present_hook ();
      initialized := true);
    sync_thy_loader ();
-   Unsynchronized.change print_mode (update (op =) ProofGeneralPgip.proof_general_emacsN);
+   Unsynchronized.change print_mode (update (op =) proof_general_emacsN);
    Secure.PG_setup ();
    Isar.toplevel_loop TextIO.stdIn
     {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 21:42:27 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 22:00:19 2013 +0200
@@ -7,21 +7,12 @@
 
 signature PROOF_GENERAL_PGIP =
 sig
-  val proof_general_emacsN: string
-
-  val new_thms_deps: theory -> theory -> string list * string list
-
   val add_preference: string -> Preferences.preference -> unit
 end
 
 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
 struct
 
-(** print mode **)
-
-val proof_general_emacsN = "ProofGeneralEmacs";
-
-
 (* assembling and issuing PGIP packets *)
 
 val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
@@ -52,40 +43,6 @@
 end;
 
 
-
-(* theorem dependencies *)
-
-local
-
-fun add_proof_body (PBody {thms, ...}) =
-  thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
-
-fun add_thm th =
-  (case Thm.proof_body_of th of
-    PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
-      if Thm.has_name_hint th andalso Thm.get_name_hint th = name
-      then add_proof_body (Future.join body)
-      else I
-  | body => add_proof_body body);
-
-in
-
-fun thms_deps ths =
-  let
-    (* FIXME proper derivation names!? *)
-    val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
-    val deps = Symtab.keys (fold add_thm ths Symtab.empty);
-  in (names, deps) end;
-
-fun new_thms_deps thy thy' =
-  let
-    val prev_facts = Global_Theory.facts_of thy;
-    val facts = Global_Theory.facts_of thy';
-  in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end;
-
-end;
-
-
 (* Preferences: tweak for PGIP interfaces *)
 
 val preferences = Unsynchronized.ref Preferences.pure_preferences;