added Isar.state/exn;
authorwenzelm
Wed, 02 Nov 2005 14:47:01 +0100
changeset 18064 f5727fa16c77
parent 18063 c4bffc47c11b
child 18065 16608ab6ed84
added Isar.state/exn;
src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Nov 02 14:47:00 2005 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Nov 02 14:47:01 2005 +0100
@@ -9,6 +9,8 @@
 sig
   structure Isar:
     sig
+      val state: unit -> Toplevel.state
+      val exn: unit -> (exn * string) option
       val main: unit -> unit
       val loop: unit -> unit
       val sync_main: unit -> unit
@@ -319,6 +321,8 @@
 
 structure Isar =
 struct
+  val state = Toplevel.get_state;
+  val exn = Toplevel.exn;
   fun main () = gen_main false false;
   fun loop () = gen_loop false false;
   fun sync_main () = gen_main true true;
@@ -340,4 +344,3 @@
 
 structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
 open BasicOuterSyntax;
-open Isar;