src/Pure/ProofGeneral/proof_general_emacs.ML
changeset 21968 883cd697112e
parent 21959 b50182aff75f
child 21970 1845e43aee93
     1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Dec 30 16:08:07 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Dec 30 16:08:09 2006 +0100
     1.3 @@ -215,16 +215,18 @@
     1.4    emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
     1.5  
     1.6  (* FIXME: check this uses non-transitive closure function here *)
     1.7 -fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
     1.8 -  let
     1.9 -    val names = filter_out (equal "") (map PureThy.get_name_hint ths);
    1.10 -    val deps = filter_out (equal "")
    1.11 -      (Symtab.keys (fold Proofterm.thms_of_proof
    1.12 -        (map Thm.proof_of ths) Symtab.empty));
    1.13 -  in
    1.14 -    if null names orelse null deps then ()
    1.15 -    else thm_deps_message (spaces_quote names, spaces_quote deps)
    1.16 -  end);
    1.17 +fun tell_thm_deps ths =
    1.18 +  if Output.has_mode thm_depsN then
    1.19 +    let
    1.20 +      val names = filter_out (equal "") (map PureThy.get_name_hint ths);
    1.21 +      val deps = filter_out (equal "")
    1.22 +        (Symtab.keys (fold Proofterm.thms_of_proof
    1.23 +          (map Thm.proof_of ths) Symtab.empty));
    1.24 +    in
    1.25 +      if null names orelse null deps then ()
    1.26 +      else thm_deps_message (spaces_quote names, spaces_quote deps)
    1.27 +    end
    1.28 +  else ();
    1.29  
    1.30  in
    1.31  
    1.32 @@ -278,25 +280,24 @@
    1.33  val initialized = ref false;
    1.34  
    1.35  fun init false =
    1.36 -      Output.panic "Proof General support no longer available for Isabelle/classic mode."
    1.37 +      Output.panic "No Proof General interface support for Isabelle/classic mode."
    1.38    | init true =
    1.39 -      (conditional (not (! initialized)) (fn () =>
    1.40 -       (setmp warning_fn (K ()) init_outer_syntax ();
    1.41 -        setup_xsymbols_output ();
    1.42 -        setup_messages ();
    1.43 -        ProofGeneralPgip.init_pgip_channel (! priority_fn);
    1.44 -        setup_state ();
    1.45 -        setup_thy_loader ();
    1.46 -        setup_present_hook ();
    1.47 -        set initialized; ()));
    1.48 -      sync_thy_loader ();
    1.49 -      change print_mode (cons proof_generalN o remove (op =) proof_generalN);
    1.50 -      ml_prompts "ML> " "ML# ";
    1.51 -      Isar.sync_main ());
    1.52 +      (! initialized orelse
    1.53 +        (setmp warning_fn (K ()) init_outer_syntax ();
    1.54 +          setup_xsymbols_output ();
    1.55 +          setup_messages ();
    1.56 +          ProofGeneralPgip.init_pgip_channel (! priority_fn);
    1.57 +          setup_state ();
    1.58 +          setup_thy_loader ();
    1.59 +          setup_present_hook ();
    1.60 +          set initialized);
    1.61 +        sync_thy_loader ();
    1.62 +       change print_mode (cons proof_generalN o remove (op =) proof_generalN);
    1.63 +       Isar.sync_main ());
    1.64  
    1.65  
    1.66  
    1.67 -(** generate elisp file for keyword classification **)
    1.68 + (** generate elisp file for keyword classification **)
    1.69  
    1.70  local
    1.71