--- 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;