# HG changeset patch
# User wenzelm
# Date 1275391925 -7200
# Node ID 54b444874be1e44f52c7a95ae3907aada95f8c47
# Parent  d94459cf7ea860258d9a961f3c6aa21036a227b7
uniform ML environment setup for Isar and PG;

diff -r d94459cf7ea8 -r 54b444874be1 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Pure/General/secure.ML	Tue Jun 01 13:32:05 2010 +0200
@@ -13,7 +13,8 @@
   val use_text: use_context -> int * string -> bool -> string -> unit
   val use_file: use_context -> bool -> string -> unit
   val toplevel_pp: string list -> string -> unit
-  val open_unsynchronized: unit -> unit
+  val Isar_setup: unit -> unit
+  val PG_setup: unit -> unit
   val commit: unit -> unit
   val bash_output: string -> string * int
   val bash: string -> int
@@ -54,7 +55,9 @@
 val use_global = raw_use_text ML_Parse.global_context (0, "") false;
 
 fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
-fun open_unsynchronized () = use_global "open Unsynchronized";
+
+fun Isar_setup () = use_global "open Unsynchronized;";
+fun PG_setup () = use_global "structure ThyLoad = Thy_Load;";
 
 
 (* shell commands *)
diff -r d94459cf7ea8 -r 54b444874be1 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jun 01 13:32:05 2010 +0200
@@ -245,6 +245,7 @@
           Unsynchronized.set initialized);
         sync_thy_loader ();
        Unsynchronized.change print_mode (update (op =) proof_generalN);
+       Secure.PG_setup ();
        Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
 end;
diff -r d94459cf7ea8 -r 54b444874be1 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Pure/ROOT.ML	Tue Jun 01 13:32:05 2010 +0200
@@ -305,11 +305,9 @@
 structure PrintMode = Print_Mode;
 structure SpecParse = Parse_Spec;
 structure ThyInfo = Thy_Info;
+structure ThyLoad = Thy_Load;
 structure ThyOutput = Thy_Output;
 structure TypeInfer = Type_Infer;
 
 end;
 
-structure ThyLoad = Thy_Load;  (*Proof General legacy*)
-
-
diff -r d94459cf7ea8 -r 54b444874be1 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Tue Jun 01 12:16:40 2010 +0200
+++ b/src/Pure/System/isar.ML	Tue Jun 01 13:32:05 2010 +0200
@@ -138,7 +138,7 @@
 
 fun toplevel_loop {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
-  Secure.open_unsynchronized ();
+  Secure.Isar_setup ();
   if do_init then init () else ();
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ());