1.1 --- a/src/Pure/ProofGeneral/preferences.ML Mon May 13 21:42:27 2013 +0200
1.2 +++ b/src/Pure/ProofGeneral/preferences.ML Mon May 13 22:00:19 2013 +0200
1.3 @@ -26,6 +26,7 @@
1.4 val nat_pref: int Unsynchronized.ref -> string -> string -> preference
1.5 val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
1.6 type T = (string * preference list) list
1.7 + val thm_depsN: string
1.8 val pure_preferences: T
1.9 val remove: string -> T -> T
1.10 val add: string -> preference -> T -> T
2.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon May 13 21:42:27 2013 +0200
2.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon May 13 22:00:19 2013 +0200
2.3 @@ -140,9 +140,34 @@
2.4 welcome ());
2.5
2.6
2.7 -(* theorem dependency output *)
2.8 +(* theorem dependencies *)
2.9
2.10 -val thm_depsN = "thm_deps";
2.11 +local
2.12 +
2.13 +fun add_proof_body (PBody {thms, ...}) =
2.14 + thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
2.15 +
2.16 +fun add_thm th =
2.17 + (case Thm.proof_body_of th of
2.18 + PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
2.19 + if Thm.has_name_hint th andalso Thm.get_name_hint th = name
2.20 + then add_proof_body (Future.join body)
2.21 + else I
2.22 + | body => add_proof_body body);
2.23 +
2.24 +in
2.25 +
2.26 +fun thm_deps ths =
2.27 + let
2.28 + (* FIXME proper derivation names!? *)
2.29 + val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
2.30 + val deps = Symtab.keys (fold add_thm ths Symtab.empty);
2.31 + in (names, deps) end;
2.32 +
2.33 +end;
2.34 +
2.35 +
2.36 +(* report theorem dependencies *)
2.37
2.38 local
2.39
2.40 @@ -154,11 +179,13 @@
2.41 in
2.42
2.43 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
2.44 - if print_mode_active thm_depsN andalso
2.45 + if print_mode_active Preferences.thm_depsN andalso
2.46 can Toplevel.theory_of state andalso Toplevel.is_theory state'
2.47 then
2.48 - let val (names, deps) =
2.49 - ProofGeneralPgip.new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state')
2.50 + let
2.51 + val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state);
2.52 + val facts = Global_Theory.facts_of (Toplevel.theory_of state');
2.53 + val (names, deps) = thm_deps (maps #2 (Facts.dest_static [prev_facts] facts));
2.54 in
2.55 if null names orelse null deps then ()
2.56 else thm_deps_message (spaces_quote names, spaces_quote deps)
2.57 @@ -205,21 +232,23 @@
2.58
2.59 (* init *)
2.60
2.61 +val proof_general_emacsN = "ProofGeneralEmacs";
2.62 +
2.63 val initialized = Unsynchronized.ref false;
2.64
2.65 fun init () =
2.66 (if ! initialized then ()
2.67 else
2.68 (Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
2.69 - Output.add_mode ProofGeneralPgip.proof_general_emacsN
2.70 + Output.add_mode proof_general_emacsN
2.71 Output.default_output Output.default_escape;
2.72 - Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
2.73 + Markup.add_mode proof_general_emacsN YXML.output_markup;
2.74 setup_messages ();
2.75 setup_thy_loader ();
2.76 setup_present_hook ();
2.77 initialized := true);
2.78 sync_thy_loader ();
2.79 - Unsynchronized.change print_mode (update (op =) ProofGeneralPgip.proof_general_emacsN);
2.80 + Unsynchronized.change print_mode (update (op =) proof_general_emacsN);
2.81 Secure.PG_setup ();
2.82 Isar.toplevel_loop TextIO.stdIn
2.83 {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
3.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 21:42:27 2013 +0200
3.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon May 13 22:00:19 2013 +0200
3.3 @@ -7,21 +7,12 @@
3.4
3.5 signature PROOF_GENERAL_PGIP =
3.6 sig
3.7 - val proof_general_emacsN: string
3.8 -
3.9 - val new_thms_deps: theory -> theory -> string list * string list
3.10 -
3.11 val add_preference: string -> Preferences.preference -> unit
3.12 end
3.13
3.14 structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
3.15 struct
3.16
3.17 -(** print mode **)
3.18 -
3.19 -val proof_general_emacsN = "ProofGeneralEmacs";
3.20 -
3.21 -
3.22 (* assembling and issuing PGIP packets *)
3.23
3.24 val pgip_refid = Unsynchronized.ref NONE: string option Unsynchronized.ref;
3.25 @@ -52,40 +43,6 @@
3.26 end;
3.27
3.28
3.29 -
3.30 -(* theorem dependencies *)
3.31 -
3.32 -local
3.33 -
3.34 -fun add_proof_body (PBody {thms, ...}) =
3.35 - thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
3.36 -
3.37 -fun add_thm th =
3.38 - (case Thm.proof_body_of th of
3.39 - PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
3.40 - if Thm.has_name_hint th andalso Thm.get_name_hint th = name
3.41 - then add_proof_body (Future.join body)
3.42 - else I
3.43 - | body => add_proof_body body);
3.44 -
3.45 -in
3.46 -
3.47 -fun thms_deps ths =
3.48 - let
3.49 - (* FIXME proper derivation names!? *)
3.50 - val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
3.51 - val deps = Symtab.keys (fold add_thm ths Symtab.empty);
3.52 - in (names, deps) end;
3.53 -
3.54 -fun new_thms_deps thy thy' =
3.55 - let
3.56 - val prev_facts = Global_Theory.facts_of thy;
3.57 - val facts = Global_Theory.facts_of thy';
3.58 - in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end;
3.59 -
3.60 -end;
3.61 -
3.62 -
3.63 (* Preferences: tweak for PGIP interfaces *)
3.64
3.65 val preferences = Unsynchronized.ref Preferences.pure_preferences;