1.1 --- a/src/Pure/Isar/outer_parse.ML	Sun Mar 26 20:10:31 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Sun Mar 26 20:11:12 2000 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    type token
     1.5    val group: string -> (token list -> 'a) -> token list -> 'a
     1.6    val !!! : (token list -> 'a) -> token list -> 'a
     1.7 +  val !!!! : (token list -> 'a) -> token list -> 'a
     1.8    val $$$ : string -> token list -> string * token list
     1.9    val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
    1.10    val command: token list -> string * token list
    1.11 @@ -86,15 +87,18 @@
    1.12  
    1.13  (* cut *)
    1.14  
    1.15 -fun !!! scan =
    1.16 +fun cut kind scan =
    1.17    let
    1.18      fun get_pos [] = " (past end-of-file!)"
    1.19        | get_pos (tok :: _) = OuterLex.pos_of tok;
    1.20  
    1.21 -    fun err (toks, None) = "Outer syntax error" ^ get_pos toks
    1.22 -      | err (toks, Some msg) = "Outer syntax error" ^ get_pos toks ^ ": " ^ msg;
    1.23 +    fun err (toks, None) = kind ^ get_pos toks
    1.24 +      | err (toks, Some msg) = kind ^ get_pos toks ^ ": " ^ msg;
    1.25    in Scan.!! err scan end;
    1.26  
    1.27 +val !!! = cut "Outer syntax error";
    1.28 +val !!!! = cut "Corrupted outer syntax in presentation";
    1.29 +
    1.30  
    1.31  
    1.32  (** basic parsers **)