improved terminator msg;
authorwenzelm
Sun Jun 04 00:00:17 2000 +0200 (2000-06-04)
changeset 9033f12d8ea8618b
parent 9032 ad0b9f048bbf
child 9034 ea4dc7603f0b
improved terminator msg;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Jun 03 23:59:37 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Jun 04 00:00:17 2000 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4    | None => sys_error ("no parser for outer syntax command " ^ quote name));
     1.5  
     1.6  fun terminator false = Scan.succeed ()
     1.7 -  | terminator true = P.group "terminator" (Scan.option P.sync -- P.$$$ ";" >> K ());
     1.8 +  | terminator true = P.group "end of input" (Scan.option P.sync -- P.$$$ ";" >> K ());
     1.9  
    1.10  in
    1.11