tuned Parse.group: delayed failure message;

--- a/src/HOL/Tools/Function/function_common.ML	Sun Aug 21 20:25:49 2011 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Aug 21 20:42:26 2011 +0200
@@ -333,7 +333,7 @@
 
 
 local
-  val option_parser = Parse.group "option"
+  val option_parser = Parse.group (fn () => "option")
     ((Parse.reserved "sequential" >> K Sequential)
      || ((Parse.reserved "default" |-- Parse.term) >> Default)
      || (Parse.reserved "domintros" >> K DomIntros)

--- a/src/Pure/Isar/args.ML	Sun Aug 21 20:25:49 2011 +0200
+++ b/src/Pure/Isar/args.ML	Sun Aug 21 20:42:26 2011 +0200
@@ -227,7 +227,7 @@
 fun parse_args is_symid =
   let
     val keyword_symid = token (Parse.keyword_with is_symid);
-    fun atom blk = Parse.group "argument"
+    fun atom blk = Parse.group (fn () => "argument")
       (ident || keyword_symid || string || alt_string || token Parse.float_number ||
         (if blk then token (Parse.$$$ ",") else Scan.fail));
 

--- a/src/Pure/Isar/outer_syntax.ML	Sun Aug 21 20:25:49 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Aug 21 20:42:26 2011 +0200
@@ -62,7 +62,9 @@
 local
 
 fun terminate false = Scan.succeed ()
-  | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
+  | terminate true =
+      Parse.group (fn () => "end of input")
+        (Scan.option Parse.sync -- Parse.semicolon >> K ());
 
 fun body cmd (name, _) =
   (case cmd name of

--- a/src/Pure/Isar/parse.ML	Sun Aug 21 20:25:49 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Sun Aug 21 20:42:26 2011 +0200
@@ -8,7 +8,7 @@
 sig
   type 'a parser = Token.T list -> 'a * Token.T list
   type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
-  val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
+  val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
   val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
   val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
   val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
@@ -114,17 +114,15 @@
 
 (* group atomic parsers (no cuts!) *)
 
-fun fail_with s = Scan.fail_with
-  (fn [] => (fn () => s ^ " expected (past end-of-file!)")
+fun group s scan = scan || Scan.fail_with
+  (fn [] => (fn () => s () ^ " expected (past end-of-file!)")
     | tok :: _ =>
         (fn () =>
           (case Token.text_of tok of
             (txt, "") =>
-              s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
+              s () ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
           | (txt1, txt2) =>
-              s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
-
-fun group s scan = scan || fail_with s;
+              s () ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
 
 
 (* cut *)
@@ -170,7 +168,8 @@
 fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
 
 fun kind k =
-  group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
+  group (fn () => Token.str_of_kind k)
+    (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
 
 val command = kind Token.Command;
 val keyword = kind Token.Keyword;
@@ -192,10 +191,11 @@
 val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
 
 fun $$$ x =
-  group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
+  group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
+    (keyword_with (fn y => x = y));
 
 fun reserved x =
-  group ("reserved identifier " ^ quote x)
+  group (fn () => "reserved identifier " ^ quote x)
     (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
 
 val semicolon = $$$ ";";
@@ -208,7 +208,7 @@
 val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
 val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
 
-val tag_name = group "tag name" (short_ident || string);
+val tag_name = group (fn () => "tag name") (short_ident || string);
 val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
 
 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
@@ -240,11 +240,17 @@
 
 (* names and text *)
 
-val name = group "name declaration" (short_ident || sym_ident || string || number);
+val name = group (fn () => "name declaration") (short_ident || sym_ident || string || number);
+
 val binding = position name >> Binding.make;
-val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
-val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
-val path = group "file name/path specification" name >> Path.explode;
+
+val xname = group (fn () => "name reference")
+  (short_ident || long_ident || sym_ident || string || number);
+
+val text = group (fn () => "text")
+  (short_ident || long_ident || sym_ident || string || number || verbatim);
+
+val path = group (fn () => "file name/path specification") name >> Path.explode;
 
 val liberal_name = keyword_ident_or_symbolic || xname;
 
@@ -254,7 +260,7 @@
 
 (* sorts and arities *)
 
-val sort = group "sort" (inner_syntax xname);
+val sort = group (fn () => "sort") (inner_syntax xname);
 
 val arity = xname -- ($$$ "::" |-- !!!
   (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
@@ -265,8 +271,9 @@
 
 (* types *)
 
-val typ_group = group "type"
-  (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
+val typ_group =
+  group (fn () => "type")
+    (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
 
 val typ = inner_syntax typ_group;
 
@@ -324,24 +331,24 @@
 
 (* embedded source text *)
 
-val ML_source = source_position (group "ML source" text);
-val doc_source = source_position (group "document source" text);
+val ML_source = source_position (group (fn () => "ML source") text);
+val doc_source = source_position (group (fn () => "document source") text);
 
 
 (* terms *)
 
 val tm = short_ident || long_ident || sym_ident || term_var || number || string;
 
-val term_group = group "term" tm;
-val prop_group = group "proposition" tm;
+val term_group = group (fn () => "term") tm;
+val prop_group = group (fn () => "proposition") tm;
 
 val term = inner_syntax term_group;
 val prop = inner_syntax prop_group;
 
-val type_const = inner_syntax (group "type constructor" xname);
-val const = inner_syntax (group "constant" xname);
+val type_const = inner_syntax (group (fn () => "type constructor") xname);
+val const = inner_syntax (group (fn () => "constant") xname);
 
-val literal_fact = inner_syntax (group "literal fact" alt_string);
+val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
 
 
 (* patterns *)

--- a/src/Pure/Isar/parse_spec.ML	Sun Aug 21 20:25:49 2011 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Sun Aug 21 20:42:26 2011 +0200
@@ -136,7 +136,7 @@
     val expr0 = plus1_unless locale_keyword expr1;
   in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
 
-val context_element = Parse.group "context element" loc_element;
+val context_element = Parse.group (fn () => "context element") loc_element;
 
 end;
 

--- a/src/Pure/Thy/thy_header.ML	Sun Aug 21 20:25:49 2011 +0200
+++ b/src/Pure/Thy/thy_header.ML	Sun Aug 21 20:42:26 2011 +0200
@@ -29,8 +29,8 @@
 
 (* header args *)
 
-val file_name = Parse.group "file name" Parse.name;
-val theory_name = Parse.group "theory name" Parse.name;
+val file_name = Parse.group (fn () => "file name") Parse.name;
+val theory_name = Parse.group (fn () => "theory name") Parse.name;
 
 val file =
   Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||