--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Sun Oct 18 21:30:01 2015 +0200
@@ -114,7 +114,7 @@
|| keyword npiN || keyword lin_denseN || keyword qeN
|| keyword atomsN || keyword simpsN;
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
val terms = thms >> map Drule.dest_term;
in
--- a/src/HOL/Decision_Procs/langford_data.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Decision_Procs/langford_data.ML Sun Oct 18 21:30:01 2015 +0200
@@ -84,7 +84,7 @@
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
val any_keyword = keyword qeN || keyword gatherN || keyword atomsN;
- val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+ val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
val terms = thms >> map Drule.dest_term;
in
--- a/src/HOL/Groebner_Basis.thy Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Groebner_Basis.thy Sun Oct 18 21:30:01 2015 +0200
@@ -41,7 +41,7 @@
val addN = "add"
val delN = "del"
val any_keyword = keyword addN || keyword delN
- val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+ val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
in
Scan.optional (keyword addN |-- thms) [] --
Scan.optional (keyword delN |-- thms) [] >>
--- a/src/HOL/Library/Reflection.thy Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Library/Reflection.thy Sun Oct 18 21:30:01 2015 +0200
@@ -22,7 +22,7 @@
val onlyN = "only";
val rulesN = "rules";
val any_keyword = keyword onlyN || keyword rulesN;
- val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+ val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
val terms = thms >> map (Thm.term_of o Drule.dest_term);
in
thms -- Scan.optional (keyword rulesN |-- thms) [] --
--- a/src/HOL/Library/rewrite.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Library/rewrite.ML Sun Oct 18 21:30:01 2015 +0200
@@ -343,7 +343,7 @@
| append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
| append_default ps = ps
- in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
+ in Scan.repeats sep_atom >> (rev #> append_default) end
fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
let
--- a/src/HOL/Presburger.thy Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Presburger.thy Sun Oct 18 21:30:01 2015 +0200
@@ -400,7 +400,7 @@
val delN = "del"
val elimN = "elim"
val any_keyword = keyword addN || keyword delN || simple_keyword elimN
- val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+ val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm)
in
Scan.optional (simple_keyword elimN >> K false) true --
Scan.optional (keyword addN |-- thms) [] --
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML Sun Oct 18 21:30:01 2015 +0200
@@ -171,7 +171,7 @@
Scan.optional (Scan.one (is_tilde o symbol) >> single) [];
val long_identifier =
- identifier @@@ (Scan.repeat1 ($$$ "." @@@ identifier) >> flat);
+ identifier @@@ Scan.repeats1 ($$$ "." @@@ identifier);
val whitespace = Scan.many (is_whitespace o symbol);
val whitespace1 = Scan.many1 (is_whitespace o symbol);
--- a/src/HOL/Tools/ATP/atp_proof.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sun Oct 18 21:30:01 2015 +0200
@@ -320,8 +320,8 @@
(parse_inference_source >> snd
|| scan_general_id --| skip_term >> single) x
and parse_dependencies x =
- (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency)
- >> (flat #> filter_out (curry (op =) "theory"))) x
+ (Scan.repeats (Scan.option ($$ ",") |-- parse_dependency)
+ >> (filter_out (curry (op =) "theory"))) x
and parse_file_source x =
(Scan.this_string "file" |-- $$ "(" |-- scan_general_id
-- Scan.option ($$ "," |-- scan_general_id
--- a/src/HOL/Tools/ATP/atp_satallax.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_satallax.ML Sun Oct 18 21:30:01 2015 +0200
@@ -405,7 +405,7 @@
#>
(if local_name <> satallaxN then
(Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
- (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat)))
+ (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem))))
#> fst)
else
(Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Sun Oct 18 21:30:01 2015 +0200
@@ -294,11 +294,10 @@
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
val parse_value =
- Scan.repeat1 (Parse.minus >> single
+ Scan.repeats1 (Parse.minus >> single
|| Scan.repeat1 (Scan.unless Parse.minus
(Parse.name || Parse.float_number))
|| @{keyword ","} |-- Parse.number >> prefix "," >> single)
- >> flat
val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []
val parse_params =
Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []
--- a/src/HOL/Tools/Qelim/cooper.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Oct 18 21:30:01 2015 +0200
@@ -897,7 +897,7 @@
val constsN = "consts";
val any_keyword = keyword constsN
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
val terms = thms >> map (Thm.term_of o Drule.dest_term);
fun optional scan = Scan.optional scan [];
--- a/src/HOL/Tools/legacy_transfer.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Tools/legacy_transfer.ML Sun Oct 18 21:30:01 2015 +0200
@@ -217,7 +217,7 @@
|| keyword_colon congN || keyword_colon labelsN
|| keyword_colon leavingN || keyword_colon directionN;
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
val names = Scan.repeat (Scan.unless any_keyword (Scan.lift Args.name))
val mode = keyword_colon modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false)
--- a/src/Pure/General/antiquote.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/General/antiquote.ML Sun Oct 18 21:30:01 2015 +0200
@@ -77,10 +77,10 @@
val err_prefix = "Antiquotation lexical error: ";
val scan_txt =
- Scan.repeat1
+ Scan.repeats1
(Scan.many1 (fn (s, _) => not (Symbol.is_control s) andalso s <> "@" andalso Symbol.not_eof s) ||
Scan.one (fn (s, _) => Symbol.is_control s) --| Scan.ahead (~$$ "\\<open>") >> single ||
- $$$ "@" --| Scan.ahead (~$$ "{")) >> flat;
+ $$$ "@" --| Scan.ahead (~$$ "{"));
val scan_antiq_body =
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
@@ -101,12 +101,12 @@
val scan_antiq =
Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos --
Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
- (Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
+ (Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
(fn (pos1, (pos2, ((body, pos3), pos4))) =>
{start = Position.set_range (pos1, pos2),
stop = Position.set_range (pos3, pos4),
range = Position.range pos1 pos4,
- body = flat body});
+ body = body});
val scan_antiquote =
scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text;
--- a/src/Pure/General/scan.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/General/scan.ML Sun Oct 18 21:30:01 2015 +0200
@@ -57,6 +57,8 @@
val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+ val repeats: ('a -> 'b list * 'a) -> 'a -> 'b list * 'a
+ val repeats1: ('a -> 'b list * 'a) -> 'a -> 'b list * 'a
val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
@@ -191,6 +193,9 @@
fun repeat1 scan = scan ::: repeat scan;
+fun repeats scan = repeat scan >> flat;
+fun repeats1 scan = repeat1 scan >> flat;
+
fun single scan = scan >> (fn x => [x]);
fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
--- a/src/Pure/General/symbol_pos.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/General/symbol_pos.ML Sun Oct 18 21:30:01 2015 +0200
@@ -118,11 +118,10 @@
fun scan_strs q err_prefix =
Scan.ahead ($$ q) |--
!!! (fn () => err_prefix ^ "unclosed string literal")
- ((scan_pos --| $$$ q) --
- ((Scan.repeat (scan_str q err_prefix) >> flat) -- ($$$ q |-- scan_pos)));
+ ((scan_pos --| $$$ q) -- (Scan.repeats (scan_str q err_prefix) -- ($$$ q |-- scan_pos)));
fun recover_strs q =
- $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q "")) >> flat);
+ $$$ q @@@ Scan.repeats (Scan.permissive (scan_str q ""));
in
@@ -202,7 +201,7 @@
Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.not_eof s)) >> single;
-val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
+val scan_cmts = Scan.pass 0 (Scan.repeats scan_cmt);
in
@@ -266,7 +265,7 @@
in
-val scan_ident = letter ::: (Scan.repeat (letdigs1 || sub ::: letdigs1) >> flat);
+val scan_ident = letter ::: Scan.repeats (letdigs1 || sub ::: letdigs1);
end;
--- a/src/Pure/Isar/attrib.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Oct 18 21:30:01 2015 +0200
@@ -281,7 +281,7 @@
val thm = gen_thm Facts.the_single;
val multi_thm = gen_thm (K I);
-val thms = Scan.repeat multi_thm >> flat;
+val thms = Scan.repeats multi_thm;
end;
--- a/src/Pure/Isar/method.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Isar/method.ML Sun Oct 18 21:30:01 2015 +0200
@@ -526,7 +526,7 @@
local
fun thms ss =
- Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
+ Scan.repeats (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm);
fun app {init, attribute, pos = _} ths context =
fold_map (Thm.apply_attribute attribute) ths (Context.map_proof init context);
--- a/src/Pure/Isar/parse.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Isar/parse.ML Sun Oct 18 21:30:01 2015 +0200
@@ -421,10 +421,7 @@
fun args blk x = Scan.optional (args1 blk) [] x
and args1 blk x =
- ((Scan.repeat1
- (Scan.repeat1 (argument blk) ||
- argsp "(" ")" ||
- argsp "[" "]")) >> flat) x
+ (Scan.repeats1 (Scan.repeat1 (argument blk) || argsp "(" ")" || argsp "[" "]")) x
and argsp l r x = (token ($$$ l) ::: !!! (args true @@@ (token ($$$ r) >> single))) x;
in (args, args1) end;
--- a/src/Pure/Isar/token.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Isar/token.ML Sun Oct 18 21:30:01 2015 +0200
@@ -551,10 +551,10 @@
Scan.ahead ($$ "{" -- $$ "*") |--
!!! "unclosed verbatim text"
((Symbol_Pos.scan_pos --| $$ "{" --| $$ "*") --
- ((Scan.repeat scan_verb >> flat) -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
+ (Scan.repeats scan_verb -- ($$ "*" |-- $$ "}" |-- Symbol_Pos.scan_pos)));
val recover_verbatim =
- $$$ "{" @@@ $$$ "*" @@@ (Scan.repeat scan_verb >> flat);
+ $$$ "{" @@@ $$$ "*" @@@ Scan.repeats scan_verb;
(* scan cartouche *)
--- a/src/Pure/ML/ml_lex.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/ML/ml_lex.ML Sun Oct 18 21:30:01 2015 +0200
@@ -198,7 +198,7 @@
val scan_ident = scan_alphanumeric || scan_symbolic;
val scan_long_ident =
- (Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "=");
+ Scan.repeats1 (scan_alphanumeric @@@ $$$ ".") @@@ (scan_ident || $$$ "=");
val scan_type_var = $$$ "'" @@@ scan_letdigs;
@@ -249,7 +249,7 @@
$$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";
-val scan_gaps = Scan.repeat scan_gap >> flat;
+val scan_gaps = Scan.repeats scan_gap;
in
@@ -262,10 +262,10 @@
val scan_string =
Scan.ahead ($$ "\"") |--
!!! "unclosed string literal"
- ($$$ "\"" @@@ (Scan.repeat (scan_gap || scan_str) >> flat) @@@ $$$ "\"");
+ ($$$ "\"" @@@ Scan.repeats (scan_gap || scan_str) @@@ $$$ "\"");
val recover_string =
- $$$ "\"" @@@ (Scan.repeat (scan_gap || Scan.permissive scan_str) >> flat);
+ $$$ "\"" @@@ Scan.repeats (scan_gap || Scan.permissive scan_str);
end;
--- a/src/Pure/PIDE/xml.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/PIDE/xml.ML Sun Oct 18 21:30:01 2015 +0200
@@ -239,12 +239,12 @@
fun parse_content xs =
(parse_optional_text @@@
- (Scan.repeat
+ Scan.repeats
((parse_element >> single ||
parse_cdata >> (single o Text) ||
parse_processing_instruction ||
parse_comment)
- @@@ parse_optional_text) >> flat)) xs
+ @@@ parse_optional_text)) xs
and parse_element xs =
($$ "<" |-- parse_name -- Scan.repeat (blanks |-- parse_att) --| blanks :--
--- a/src/Pure/Syntax/lexicon.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Syntax/lexicon.ML Sun Oct 18 21:30:01 2015 +0200
@@ -94,7 +94,7 @@
fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
val scan_id = Symbol_Pos.scan_ident;
-val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
+val scan_longid = scan_id @@@ Scan.repeats1 ($$$ "." @@@ scan_id);
val scan_tid = $$$ "'" @@@ scan_id;
val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
@@ -238,12 +238,12 @@
val scan_str =
Scan.ahead ($$ "'" -- $$ "'") |--
!!! "unclosed string literal"
- ($$$ "'" @@@ $$$ "'" @@@ (Scan.repeat scan_chr >> flat) @@@ $$$ "'" @@@ $$$ "'");
+ ($$$ "'" @@@ $$$ "'" @@@ Scan.repeats scan_chr @@@ $$$ "'" @@@ $$$ "'");
val scan_str_body =
Scan.ahead ($$ "'" |-- $$ "'") |--
!!! "unclosed string literal"
- ($$ "'" |-- $$ "'" |-- (Scan.repeat scan_chr >> flat) --| $$ "'" --| $$ "'");
+ ($$ "'" |-- $$ "'" |-- Scan.repeats scan_chr --| $$ "'" --| $$ "'");
fun implode_str ss = enclose "''" "''" (implode (map (fn "'" => "\\'" | s => s) ss));
val explode_str = explode_literal scan_str_body;
--- a/src/Pure/Tools/rail.ML Sun Oct 18 20:48:24 2015 +0200
+++ b/src/Pure/Tools/rail.ML Sun Oct 18 21:30:01 2015 +0200
@@ -104,7 +104,7 @@
[Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
val scan =
- (Scan.repeat scan_token >> flat) --|
+ Scan.repeats scan_token --|
Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
(Scan.ahead (Scan.one Symbol_Pos.is_eof));