# HG changeset patch
# User wenzelm
# Date 1114278651 -7200
# Node ID 74d8412b1a27cd7d2740354adf221208a21ebdc0
# Parent  652e53c4a1ed945fa2df8d88ebbf6574c4d89003
added structure Isar (from isar.ML);

diff -r 652e53c4a1ed -r 74d8412b1a27 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 23 19:50:40 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sat Apr 23 19:50:51 2005 +0200
@@ -7,10 +7,13 @@
 
 signature BASIC_OUTER_SYNTAX =
 sig
-  val main: unit -> unit
-  val loop: unit -> unit
-  val sync_main: unit -> unit
-  val sync_loop: unit -> unit
+  structure Isar:
+    sig
+      val main: unit -> unit
+      val loop: unit -> unit
+      val sync_main: unit -> unit
+      val sync_loop: unit -> unit
+    end;
 end;
 
 signature OUTER_SYNTAX =
@@ -376,10 +379,13 @@
   writeln (Session.welcome ());
   gen_loop term no_pos);
 
-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;
+structure Isar =
+struct
+  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;
 
 
 (*final declarations of this structure!*)
@@ -387,7 +393,6 @@
 val markup_command = parser false o SOME;
 val improper_command = parser true NONE;
 
-
 end;
 
 (*setup theory syntax dependent operations*)
@@ -397,3 +402,4 @@
 
 structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
 open BasicOuterSyntax;
+open Isar;