# HG changeset patch
# User wenzelm
# Date 954094272 -7200
# Node ID 5c7ed2af8bfbd0d2c68d9979d7835f28ccf120d9
# Parent  e79ee31d3936e38331665188f3abb2dadd55886b
!!!! = cut "Corrupted outer syntax in presentation";

diff -r e79ee31d3936 -r 5c7ed2af8bfb src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sun Mar 26 20:10:31 2000 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Sun Mar 26 20:11:12 2000 +0200
@@ -10,6 +10,7 @@
   type token
   val group: string -> (token list -> 'a) -> token list -> 'a
   val !!! : (token list -> 'a) -> token list -> 'a
+  val !!!! : (token list -> 'a) -> token list -> 'a
   val $$$ : string -> token list -> string * token list
   val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
   val command: token list -> string * token list
@@ -86,15 +87,18 @@
 
 (* cut *)
 
-fun !!! scan =
+fun cut kind scan =
   let
     fun get_pos [] = " (past end-of-file!)"
       | get_pos (tok :: _) = OuterLex.pos_of tok;
 
-    fun err (toks, None) = "Outer syntax error" ^ get_pos toks
-      | err (toks, Some msg) = "Outer syntax error" ^ get_pos toks ^ ": " ^ msg;
+    fun err (toks, None) = kind ^ get_pos toks
+      | err (toks, Some msg) = kind ^ get_pos toks ^ ": " ^ msg;
   in Scan.!! err scan end;
 
+val !!! = cut "Outer syntax error";
+val !!!! = cut "Corrupted outer syntax in presentation";
+
 
 
 (** basic parsers **)