added Isar.state/exn;
authorwenzelm
Wed Nov 02 14:47:01 2005 +0100 (2005-11-02)
changeset 18064f5727fa16c77
parent 18063 c4bffc47c11b
child 18065 16608ab6ed84
added Isar.state/exn;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Nov 02 14:47:00 2005 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Nov 02 14:47:01 2005 +0100
     1.3 @@ -9,6 +9,8 @@
     1.4  sig
     1.5    structure Isar:
     1.6      sig
     1.7 +      val state: unit -> Toplevel.state
     1.8 +      val exn: unit -> (exn * string) option
     1.9        val main: unit -> unit
    1.10        val loop: unit -> unit
    1.11        val sync_main: unit -> unit
    1.12 @@ -319,6 +321,8 @@
    1.13  
    1.14  structure Isar =
    1.15  struct
    1.16 +  val state = Toplevel.get_state;
    1.17 +  val exn = Toplevel.exn;
    1.18    fun main () = gen_main false false;
    1.19    fun loop () = gen_loop false false;
    1.20    fun sync_main () = gen_main true true;
    1.21 @@ -340,4 +344,3 @@
    1.22  
    1.23  structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
    1.24  open BasicOuterSyntax;
    1.25 -open Isar;