# HG changeset patch # User wenzelm # Date 1152192093 -7200 # Node ID 33124a9f5e31d71ec3e55184715c1a11944b9a4f # Parent b07a138b4e7d1355f311b5a4c911299660205924 added Isar.context; diff -r b07a138b4e7d -r 33124a9f5e31 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Thu Jul 06 12:18:17 2006 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Thu Jul 06 15:21:33 2006 +0200 @@ -10,6 +10,7 @@ structure Isar: sig val state: unit -> Toplevel.state + val context: unit -> Proof.context val exn: unit -> (exn * string) option val main: unit -> unit val loop: unit -> unit @@ -323,6 +324,7 @@ structure Isar = struct val state = Toplevel.get_state; + val context = Context.proof_of o Toplevel.context_of o state; val exn = Toplevel.exn; fun main () = gen_main false false; fun loop () = gen_loop false false;