src/Pure/ProofGeneral/proof_general_emacs.ML
changeset 21948 e34bc5e4e7bc
parent 21945 4dd9a5fc7fc3
child 21959 b50182aff75f
     1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 29 19:50:48 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Dec 29 19:50:50 2006 +0100
     1.3 @@ -9,7 +9,6 @@
     1.4  signature PROOF_GENERAL =
     1.5  sig
     1.6    val init: bool -> unit
     1.7 -  val init_pgip: bool -> unit           (* for compatibility; always fails *)
     1.8    val write_keywords: string -> unit
     1.9  end;
    1.10  
    1.11 @@ -68,7 +67,7 @@
    1.12  fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
    1.13  
    1.14  fun tagit (kind, bg_tag) x =
    1.15 -    (bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
    1.16 +  (bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
    1.17  
    1.18  fun free_or_skolem x =
    1.19    (case try Name.dest_skolem x of
    1.20 @@ -147,10 +146,10 @@
    1.21  in
    1.22  
    1.23  fun setup_state () =
    1.24 -  (Display.print_current_goals_fn := print_current_goals;
    1.25 -   Toplevel.print_state_fn := print_state;
    1.26 -   Toplevel.prompt_state_fn :=
    1.27 -     (fn s => suffix (special "372") (Toplevel.prompt_state_default s)));
    1.28 + (Display.print_current_goals_fn := print_current_goals;
    1.29 +  Toplevel.print_state_fn := print_state;
    1.30 +  Toplevel.prompt_state_fn :=
    1.31 +    (fn s => suffix (special "372") (Toplevel.prompt_state_default s)));
    1.32  
    1.33  end;
    1.34  
    1.35 @@ -172,29 +171,10 @@
    1.36  end;
    1.37  
    1.38  
    1.39 -(* prepare theory context *)
    1.40 +(* get informed about files *)
    1.41  
    1.42  val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
    1.43  
    1.44 -(* FIXME general treatment of tracing*)
    1.45 -val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
    1.46 -
    1.47 -fun dynamic_context () =
    1.48 -  (case Context.get_context () of
    1.49 -    SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
    1.50 -  | NONE => "");
    1.51 -
    1.52 -fun try_update_thy_only file =
    1.53 -  ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
    1.54 -    let val name = thy_name file in
    1.55 -      if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
    1.56 -      then update_thy_only name
    1.57 -      else warning ("Unkown theory context of ML file." ^ dynamic_context ())
    1.58 -    end) ();
    1.59 -
    1.60 -
    1.61 -(* get informed about files *)
    1.62 -
    1.63  val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
    1.64  val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
    1.65  val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
    1.66 @@ -233,7 +213,7 @@
    1.67  val spaces_quote = space_implode " " o map quote;
    1.68  
    1.69  fun thm_deps_message (thms, deps) =
    1.70 -    emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
    1.71 +  emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
    1.72  
    1.73  (* FIXME: check this uses non-transitive closure function here *)
    1.74  fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
    1.75 @@ -263,19 +243,6 @@
    1.76    OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
    1.77      (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
    1.78  
    1.79 -val redoP = (*redo without output*)
    1.80 -  OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
    1.81 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
    1.82 -
    1.83 -val context_thy_onlyP =
    1.84 -  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
    1.85 -    (P.name >> (Toplevel.no_timing oo IsarCmd.init_context update_thy_only));
    1.86 -
    1.87 -val try_context_thy_onlyP =
    1.88 -  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
    1.89 -    (P.name >> (Toplevel.no_timing oo
    1.90 -      (Toplevel.imperative (K ()) oo IsarCmd.init_context try_update_thy_only)));
    1.91 -
    1.92  val restartP =
    1.93    OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
    1.94      (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
    1.95 @@ -302,8 +269,7 @@
    1.96        (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
    1.97  
    1.98  fun init_outer_syntax () = OuterSyntax.add_parsers
    1.99 - [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
   1.100 -  inform_file_processedP, inform_file_retractedP, process_pgipP];
   1.101 + [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
   1.102  
   1.103  end;
   1.104  
   1.105 @@ -313,7 +279,7 @@
   1.106  val initialized = ref false;
   1.107  
   1.108  fun init false =
   1.109 -      Output.panic "Interface support no longer available for Isabelle/classic mode."
   1.110 +      Output.panic "Proof General support no longer available for Isabelle/classic mode."
   1.111    | init true =
   1.112        (conditional (not (! initialized)) (fn () =>
   1.113         (setmp warning_fn (K ()) init_outer_syntax ();
   1.114 @@ -329,9 +295,6 @@
   1.115        ml_prompts "ML> " "ML# ";
   1.116        Isar.sync_main ());
   1.117  
   1.118 -fun init_pgip false = init true
   1.119 -  | init_pgip true = Output.panic "No PGIP here, please use ProofGeneralPgip.init_pgip."
   1.120 -
   1.121  
   1.122  
   1.123  (** generate elisp file for keyword classification **)