src/Pure/Isar/outer_syntax.ML

 
 signature BASIC_OUTER_SYNTAX =
 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
       val sync_loop: unit -> unit
     end;

   writeln (Session.welcome ());
   gen_loop term no_pos);
 
 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;
   fun sync_loop () = gen_loop true true;
 end;

 ThyLoad.load_thy_fn := OuterSyntax.load_thy;
 structure ThyLoad: THY_LOAD = ThyLoad;
 
 structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
 open BasicOuterSyntax;
-open Isar;