# HG changeset patch
# User wenzelm
# Date 1207826660 -7200
# Node ID 410d02ea13c9853d89d8ac92a1e1dfec0bdb5886
# Parent  5534b6a6b810466d1200de6949db3d848ed73f49
moved global Toplevel state to structure Isar;

diff -r 5534b6a6b810 -r 410d02ea13c9 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 13:24:19 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 13:24:20 2008 +0200
@@ -485,7 +485,7 @@
     s |> OuterSyntax.scan |> OuterSyntax.read
       (*|> map (Toplevel.position Position.none o #3)*)
       |> map #3
-      |> Toplevel.>>>;
+      |> Isar.>>>;
 
 (* TODO:
     - apply a command given a transition function, e.g. IsarCmd.undo.
@@ -710,7 +710,7 @@
             let
                 (* TODO: interim: this is probably not right.
                    What we want is mapping onto simple PGIP name/context model. *)
-                val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
+                val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
                 val thy = Context.theory_of_proof ctx
                 val ths = [PureThy.get_thm thy thmname]
                 val deps = filter_out (equal "")
@@ -739,7 +739,7 @@
         val objtype = #objtype vs
         val name = #name vs
 
-        val topthy = Toplevel.theory_of o Toplevel.get_state
+        val topthy = Toplevel.theory_of o Isar.state
 
         fun splitthy id =
             let val comps = NameSpace.explode id
@@ -796,7 +796,7 @@
     let
         val openfile = !currently_open_file
 
-        val topthy = Toplevel.theory_of o Toplevel.get_state
+        val topthy = Toplevel.theory_of o Isar.state
         val topthy_name = Context.theory_name o topthy
 
         val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE