# HG changeset patch # User wenzelm # Date 1384620721 -3600 # Node ID 7815563f50dc3c274c64718057c5bd9562dd6383 # Parent f3cfe882f9afe5044e6dae8010a7f09a0701f303 tuned signature -- clarified Proof General legacy; diff -r f3cfe882f9af -r 7815563f50dc src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Sat Nov 16 17:39:11 2013 +0100 +++ b/src/Pure/Thy/thy_load.ML Sat Nov 16 17:52:01 2013 +0100 @@ -21,8 +21,6 @@ val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val load_thy: (Toplevel.transition -> Time.time option) -> int -> Path.T -> Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int - val set_master_path: Path.T -> unit - val get_master_path: unit -> Path.T end; structure Thy_Load: THY_LOAD = @@ -260,16 +258,4 @@ |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}") end)); - -(* global master path *) (*Proof General legacy*) - -local - val master_path = Unsynchronized.ref Path.current; -in - -fun set_master_path path = master_path := path; -fun get_master_path () = ! master_path; - end; - -end; diff -r f3cfe882f9af -r 7815563f50dc src/Pure/Tools/proof_general.ML --- a/src/Pure/Tools/proof_general.ML Sat Nov 16 17:39:11 2013 +0100 +++ b/src/Pure/Tools/proof_general.ML Sat Nov 16 17:52:01 2013 +0100 @@ -36,6 +36,7 @@ val tell_clear_response: unit -> unit val inform_file_processed: string -> unit val inform_file_retracted: string -> unit + val master_path: Path.T Unsynchronized.ref structure ThyLoad: sig val add_path: string -> unit end val thm_deps: bool Unsynchronized.ref val proof_generalN: string @@ -293,11 +294,14 @@ (** theory loader **) -(* fake old ThyLoad -- with new semantics *) +(* global master path *) +val master_path = Unsynchronized.ref Path.current; + +(*fake old ThyLoad -- with new semantics*) structure ThyLoad = struct - val add_path = Thy_Load.set_master_path o Path.explode; + fun add_path path = master_path := Path.explode path; end; diff -r f3cfe882f9af -r 7815563f50dc src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Sat Nov 16 17:39:11 2013 +0100 +++ b/src/Pure/pure_syn.ML Sat Nov 16 17:52:01 2013 +0100 @@ -14,7 +14,7 @@ (Thy_Header.args >> (fn header => Toplevel.print o Toplevel.init_theory - (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header))); + (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header))); val _ = Outer_Syntax.command