tuned Parse.group: delayed failure message;
authorwenzelm
Sun Aug 21 20:42:26 2011 +0200 (2011-08-21)
changeset 443575f5649ac8235
parent 44356 f6a2e5ce2ce5
child 44358 2a2df4de1bbe
tuned Parse.group: delayed failure message;
src/HOL/Tools/Function/function_common.ML
src/Pure/Isar/args.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Thy/thy_header.ML
     1.1 --- a/src/HOL/Tools/Function/function_common.ML	Sun Aug 21 20:25:49 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sun Aug 21 20:42:26 2011 +0200
     1.3 @@ -333,7 +333,7 @@
     1.4  
     1.5  
     1.6  local
     1.7 -  val option_parser = Parse.group "option"
     1.8 +  val option_parser = Parse.group (fn () => "option")
     1.9      ((Parse.reserved "sequential" >> K Sequential)
    1.10       || ((Parse.reserved "default" |-- Parse.term) >> Default)
    1.11       || (Parse.reserved "domintros" >> K DomIntros)
     2.1 --- a/src/Pure/Isar/args.ML	Sun Aug 21 20:25:49 2011 +0200
     2.2 +++ b/src/Pure/Isar/args.ML	Sun Aug 21 20:42:26 2011 +0200
     2.3 @@ -227,7 +227,7 @@
     2.4  fun parse_args is_symid =
     2.5    let
     2.6      val keyword_symid = token (Parse.keyword_with is_symid);
     2.7 -    fun atom blk = Parse.group "argument"
     2.8 +    fun atom blk = Parse.group (fn () => "argument")
     2.9        (ident || keyword_symid || string || alt_string || token Parse.float_number ||
    2.10          (if blk then token (Parse.$$$ ",") else Scan.fail));
    2.11  
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Aug 21 20:25:49 2011 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Aug 21 20:42:26 2011 +0200
     3.3 @@ -62,7 +62,9 @@
     3.4  local
     3.5  
     3.6  fun terminate false = Scan.succeed ()
     3.7 -  | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
     3.8 +  | terminate true =
     3.9 +      Parse.group (fn () => "end of input")
    3.10 +        (Scan.option Parse.sync -- Parse.semicolon >> K ());
    3.11  
    3.12  fun body cmd (name, _) =
    3.13    (case cmd name of
     4.1 --- a/src/Pure/Isar/parse.ML	Sun Aug 21 20:25:49 2011 +0200
     4.2 +++ b/src/Pure/Isar/parse.ML	Sun Aug 21 20:42:26 2011 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  sig
     4.5    type 'a parser = Token.T list -> 'a * Token.T list
     4.6    type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
     4.7 -  val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
     4.8 +  val group: (unit -> string) -> (Token.T list -> 'a) -> Token.T list -> 'a
     4.9    val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
    4.10    val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
    4.11    val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
    4.12 @@ -114,17 +114,15 @@
    4.13  
    4.14  (* group atomic parsers (no cuts!) *)
    4.15  
    4.16 -fun fail_with s = Scan.fail_with
    4.17 -  (fn [] => (fn () => s ^ " expected (past end-of-file!)")
    4.18 +fun group s scan = scan || Scan.fail_with
    4.19 +  (fn [] => (fn () => s () ^ " expected (past end-of-file!)")
    4.20      | tok :: _ =>
    4.21          (fn () =>
    4.22            (case Token.text_of tok of
    4.23              (txt, "") =>
    4.24 -              s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
    4.25 +              s () ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
    4.26            | (txt1, txt2) =>
    4.27 -              s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
    4.28 -
    4.29 -fun group s scan = scan || fail_with s;
    4.30 +              s () ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2)));
    4.31  
    4.32  
    4.33  (* cut *)
    4.34 @@ -170,7 +168,8 @@
    4.35  fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
    4.36  
    4.37  fun kind k =
    4.38 -  group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
    4.39 +  group (fn () => Token.str_of_kind k)
    4.40 +    (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
    4.41  
    4.42  val command = kind Token.Command;
    4.43  val keyword = kind Token.Keyword;
    4.44 @@ -192,10 +191,11 @@
    4.45  val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
    4.46  
    4.47  fun $$$ x =
    4.48 -  group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
    4.49 +  group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
    4.50 +    (keyword_with (fn y => x = y));
    4.51  
    4.52  fun reserved x =
    4.53 -  group ("reserved identifier " ^ quote x)
    4.54 +  group (fn () => "reserved identifier " ^ quote x)
    4.55      (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
    4.56  
    4.57  val semicolon = $$$ ";";
    4.58 @@ -208,7 +208,7 @@
    4.59  val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
    4.60  val real = float_number >> (the o Real.fromString) || int >> Real.fromInt;
    4.61  
    4.62 -val tag_name = group "tag name" (short_ident || string);
    4.63 +val tag_name = group (fn () => "tag name") (short_ident || string);
    4.64  val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
    4.65  
    4.66  val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
    4.67 @@ -240,11 +240,17 @@
    4.68  
    4.69  (* names and text *)
    4.70  
    4.71 -val name = group "name declaration" (short_ident || sym_ident || string || number);
    4.72 +val name = group (fn () => "name declaration") (short_ident || sym_ident || string || number);
    4.73 +
    4.74  val binding = position name >> Binding.make;
    4.75 -val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
    4.76 -val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    4.77 -val path = group "file name/path specification" name >> Path.explode;
    4.78 +
    4.79 +val xname = group (fn () => "name reference")
    4.80 +  (short_ident || long_ident || sym_ident || string || number);
    4.81 +
    4.82 +val text = group (fn () => "text")
    4.83 +  (short_ident || long_ident || sym_ident || string || number || verbatim);
    4.84 +
    4.85 +val path = group (fn () => "file name/path specification") name >> Path.explode;
    4.86  
    4.87  val liberal_name = keyword_ident_or_symbolic || xname;
    4.88  
    4.89 @@ -254,7 +260,7 @@
    4.90  
    4.91  (* sorts and arities *)
    4.92  
    4.93 -val sort = group "sort" (inner_syntax xname);
    4.94 +val sort = group (fn () => "sort") (inner_syntax xname);
    4.95  
    4.96  val arity = xname -- ($$$ "::" |-- !!!
    4.97    (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
    4.98 @@ -265,8 +271,9 @@
    4.99  
   4.100  (* types *)
   4.101  
   4.102 -val typ_group = group "type"
   4.103 -  (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
   4.104 +val typ_group =
   4.105 +  group (fn () => "type")
   4.106 +    (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
   4.107  
   4.108  val typ = inner_syntax typ_group;
   4.109  
   4.110 @@ -324,24 +331,24 @@
   4.111  
   4.112  (* embedded source text *)
   4.113  
   4.114 -val ML_source = source_position (group "ML source" text);
   4.115 -val doc_source = source_position (group "document source" text);
   4.116 +val ML_source = source_position (group (fn () => "ML source") text);
   4.117 +val doc_source = source_position (group (fn () => "document source") text);
   4.118  
   4.119  
   4.120  (* terms *)
   4.121  
   4.122  val tm = short_ident || long_ident || sym_ident || term_var || number || string;
   4.123  
   4.124 -val term_group = group "term" tm;
   4.125 -val prop_group = group "proposition" tm;
   4.126 +val term_group = group (fn () => "term") tm;
   4.127 +val prop_group = group (fn () => "proposition") tm;
   4.128  
   4.129  val term = inner_syntax term_group;
   4.130  val prop = inner_syntax prop_group;
   4.131  
   4.132 -val type_const = inner_syntax (group "type constructor" xname);
   4.133 -val const = inner_syntax (group "constant" xname);
   4.134 +val type_const = inner_syntax (group (fn () => "type constructor") xname);
   4.135 +val const = inner_syntax (group (fn () => "constant") xname);
   4.136  
   4.137 -val literal_fact = inner_syntax (group "literal fact" alt_string);
   4.138 +val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
   4.139  
   4.140  
   4.141  (* patterns *)
     5.1 --- a/src/Pure/Isar/parse_spec.ML	Sun Aug 21 20:25:49 2011 +0200
     5.2 +++ b/src/Pure/Isar/parse_spec.ML	Sun Aug 21 20:42:26 2011 +0200
     5.3 @@ -136,7 +136,7 @@
     5.4      val expr0 = plus1_unless locale_keyword expr1;
     5.5    in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
     5.6  
     5.7 -val context_element = Parse.group "context element" loc_element;
     5.8 +val context_element = Parse.group (fn () => "context element") loc_element;
     5.9  
    5.10  end;
    5.11  
     6.1 --- a/src/Pure/Thy/thy_header.ML	Sun Aug 21 20:25:49 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Aug 21 20:42:26 2011 +0200
     6.3 @@ -29,8 +29,8 @@
     6.4  
     6.5  (* header args *)
     6.6  
     6.7 -val file_name = Parse.group "file name" Parse.name;
     6.8 -val theory_name = Parse.group "theory name" Parse.name;
     6.9 +val file_name = Parse.group (fn () => "file name") Parse.name;
    6.10 +val theory_name = Parse.group (fn () => "theory name") Parse.name;
    6.11  
    6.12  val file =
    6.13    Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||