# HG changeset patch
# User wenzelm
# Date 921674361 -3600
# Node ID 47b357194f328ffbfc0926844187b0bc0ad4f1d2
# Parent  44b104595441d84d56d795ab22e5176f1e846bed
added (improper_)command;

diff -r 44b104595441 -r 47b357194f32 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Mar 17 13:39:01 1999 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Mar 17 13:39:21 1999 +0100
@@ -23,6 +23,10 @@
   type parser
   val parser: bool -> string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
+  val command: string -> string ->
+    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
+  val improper_command: string -> string ->
+    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val print_outer_syntax: unit -> unit
   val commands: unit -> string list
   val add_keywords: string list -> unit
@@ -49,6 +53,9 @@
 
 fun parser int_only name comment parse = Parser (name, comment, int_only, parse);
 
+val command_parser = parser false;
+val improper_command_parser = parser true;
+
 
 (* parse command *)
 
@@ -289,6 +296,10 @@
     \invoke 'loop();' to enter the Isar loop.");
 
 
+(*final declarations of this structure!*)
+val command = command_parser;
+val improper_command = improper_command_parser;
+
 end;
 
 (*setup theory syntax dependent operations*)