removed obsolete context_thy etc.;
authorwenzelm
Fri Dec 29 19:50:51 2006 +0100 (2006-12-29)
changeset 21949046e0482f0a1
parent 21948 e34bc5e4e7bc
child 21950 e97fd6480091
removed obsolete context_thy etc.;
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Dec 29 19:50:50 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Dec 29 19:50:51 2006 +0100
     1.3 @@ -6,7 +6,6 @@
     1.4  See http://proofgeneral.inf.ed.ac.uk/kit
     1.5  *)
     1.6  
     1.7 -
     1.8  signature PROOF_GENERAL_PGIP =
     1.9  sig
    1.10    val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
    1.11 @@ -23,6 +22,7 @@
    1.12  
    1.13  open Pgip;
    1.14  
    1.15 +
    1.16  (* print modes *)
    1.17  
    1.18  val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
    1.19 @@ -84,7 +84,7 @@
    1.20  fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
    1.21  
    1.22  fun tagit kind x =
    1.23 - (xml_atom kind x, real (Symbol.length (Symbol.explode x)));
    1.24 +  (xml_atom kind x, real (Symbol.length (Symbol.explode x)));
    1.25  
    1.26  fun free_or_skolem x =
    1.27    (case try Name.dest_skolem x of
    1.28 @@ -266,29 +266,10 @@
    1.29  end;
    1.30  
    1.31  
    1.32 -(* prepare theory context *)
    1.33 +(* get informed about files *)
    1.34  
    1.35  val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
    1.36  
    1.37 -(* FIXME general treatment of tracing*)
    1.38 -val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
    1.39 -
    1.40 -fun dynamic_context () =
    1.41 -  (case Context.get_context () of
    1.42 -    SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
    1.43 -  | NONE => "");
    1.44 -
    1.45 -fun try_update_thy_only file =
    1.46 -  ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
    1.47 -    let val name = thy_name file in
    1.48 -      if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
    1.49 -      then update_thy_only name
    1.50 -      else warning ("Unkown theory context of ML file." ^ dynamic_context ())
    1.51 -    end) ();
    1.52 -
    1.53 -
    1.54 -(* get informed about files *)
    1.55 -
    1.56  val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
    1.57  val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
    1.58  
    1.59 @@ -954,16 +935,6 @@
    1.60    OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
    1.61      (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
    1.62  
    1.63 -(* da: what were these context commands ones for? *)
    1.64 -val context_thy_onlyP =
    1.65 -  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
    1.66 -    (P.name >> (Toplevel.no_timing oo IsarCmd.init_context update_thy_only));
    1.67 -
    1.68 -val try_context_thy_onlyP =
    1.69 -  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
    1.70 -    (P.name >> (Toplevel.no_timing oo
    1.71 -      (Toplevel.imperative (K ()) oo IsarCmd.init_context try_update_thy_only)));
    1.72 -
    1.73  (* ProofGeneral.kill_proof still used above *)
    1.74  val kill_proofP =
    1.75    OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
    1.76 @@ -989,8 +960,7 @@
    1.77        (fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
    1.78  
    1.79  fun init_outer_syntax () = OuterSyntax.add_parsers
    1.80 - [undoP, redoP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
    1.81 -  inform_file_processedP, inform_file_retractedP, process_pgipP];
    1.82 + [undoP, redoP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
    1.83  
    1.84  end;
    1.85