1.1 --- a/src/Pure/Interface/proof_general.ML	Wed Oct 27 17:25:53 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Wed Oct 27 17:27:07 1999 +0200
     1.3 @@ -8,14 +8,16 @@
     1.4  signature PROOF_GENERAL =
     1.5  sig
     1.6    val setup: (theory -> theory) list
     1.7 +  val update_thy_only: string -> unit
     1.8 +  val try_update_thy_only: string -> unit
     1.9 +  val inform_file_processed: string -> unit
    1.10 +  val inform_file_retracted: string -> unit
    1.11    val thms_containing: xstring list -> unit
    1.12    val help: unit -> unit
    1.13    val show_context: unit -> theory
    1.14    val kill_goal: unit -> unit
    1.15    val repeat_undo: int -> unit
    1.16    val isa_restart: unit -> unit
    1.17 -  val inform_file_processed: string -> unit
    1.18 -  val inform_file_retracted: string -> unit
    1.19    val init: bool -> unit
    1.20    val write_keywords: unit -> unit
    1.21  end;
    1.22 @@ -126,9 +128,26 @@
    1.23  end;
    1.24  
    1.25  
    1.26 -(* get informed about files *)
    1.27 +(* prepare theory context *)
    1.28  
    1.29  val thy_name = Path.pack o Path.drop_ext o Path.base o Path.unpack;
    1.30 +val update_thy_only = ThyInfo.update_thy_only;
    1.31 +
    1.32 +fun which_context () =
    1.33 +  (case Context.get_context () of
    1.34 +    Some thy => "  Using current (dynamic!) one: " ^
    1.35 +      (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>") ^ "."
    1.36 +  | None => "");
    1.37 +
    1.38 +fun try_update_thy_only file =
    1.39 +  ThyLoad.cond_with_path (Path.dir (Path.unpack file)) (fn () =>
    1.40 +    let val name = thy_name file in
    1.41 +      if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
    1.42 +      else warning ("Unkown theory context of ML file." ^ which_context ())
    1.43 +    end) ();
    1.44 +
    1.45 +
    1.46 +(* get informed about files *)
    1.47  
    1.48  (* FIXME improve, e.g. do something like pretend_use_thy *)
    1.49  fun inform_file_processed file =
    1.50 @@ -176,6 +195,14 @@
    1.51  
    1.52  local structure P = OuterParse and K = OuterSyntax.Keyword in
    1.53  
    1.54 +val context_thy_onlyP =
    1.55 +  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
    1.56 +    (P.name >> IsarThy.init_context update_thy_only);
    1.57 +
    1.58 +val try_context_thy_onlyP =
    1.59 +  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
    1.60 +    (P.name >> IsarThy.init_context try_update_thy_only);
    1.61 +
    1.62  val restartP =
    1.63    OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
    1.64      (P.opt_unit >> K (Toplevel.imperative isar_restart));
    1.65 @@ -192,8 +219,9 @@
    1.66    OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
    1.67      (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name)));
    1.68  
    1.69 -fun init_outer_syntax () =
    1.70 -  OuterSyntax.add_parsers [restartP, kill_proofP, inform_file_processedP, inform_file_retractedP];
    1.71 +fun init_outer_syntax () = OuterSyntax.add_parsers
    1.72 + [restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
    1.73 +  inform_file_processedP, inform_file_retractedP];
    1.74  
    1.75  end;
    1.76