added ::: / @@@ scanner combinators;

--- a/src/HOL/Statespace/state_space.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/HOL/Statespace/state_space.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -701,7 +701,7 @@
 
 val comp = P.name -- (P.$$$ "::" |-- P.!!! P.typ);
 fun plus1_unless test scan =
-  scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::;
+  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
 
 val mapsto = P.$$$ "=";
 val rename = P.name -- (mapsto |-- P.name);

--- a/src/HOL/Tools/res_reconstruct.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -70,7 +70,7 @@
 val integer = Scan.many1 is_digit >> (valOf o Int.fromString o implode);
 
 (*Generalized FO terms, which include filenames, numbers, etc.*)
-fun termlist x = (term -- Scan.repeat ($$"," |-- term) >> op::) x
+fun termlist x = (term ::: Scan.repeat ($$"," |-- term)) x
 and term x = (quoted >> atom || integer>>Int || truefalse ||
               Symbol.scan_id -- Scan.optional ($$"(" |-- termlist --| $$")") [] >> Br ||
               $$"(" |-- term --| $$")" ||
@@ -88,7 +88,7 @@
 fun literal x = ($$"~" |-- literal >> negate ||
                  (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal)) x;
 
-val literals = literal -- Scan.repeat ($$"|" |-- literal) >> op:: ;
+val literals = literal ::: Scan.repeat ($$"|" |-- literal);
 
 (*Clause: a list of literals separated by the disjunction sign*)
 val clause = $$"(" |-- literals --| $$")" || Scan.single literal;

--- a/src/Pure/General/scan.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/Pure/General/scan.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -6,6 +6,7 @@
 *)
 
 infix 5 -- :-- :|-- |-- --| ^^;
+infixr 5 ::: @@@;
 infix 3 >>;
 infixr 0 ||;
 
@@ -27,6 +28,8 @@
   val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
   (*concatenation*)
   val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
+  val ::: : ('a -> 'b * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd
+  val @@@ : ('a -> 'b list * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd
   (*one element literal*)
   val $$ : string -> string list -> string * string list
   val ~$$ : string -> string list -> string * string list
@@ -120,6 +123,8 @@
 fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
 fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
 fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
+fun (scan1 ::: scan2) = scan1 -- scan2 >> op ::;
+fun (scan1 @@@ scan2) = scan1 -- scan2 >> op @;
 
 
 (* generic scanners *)
@@ -154,7 +159,7 @@
       if pred x then apfst (cons x) (many pred xs)
       else ([], lst);
 
-fun many1 pred = one pred -- many pred >> op ::;
+fun many1 pred = one pred ::: many pred;
 
 fun optional scan def = scan || succeed def;
 fun option scan = (scan >> SOME) || succeed NONE;
@@ -167,7 +172,7 @@
       | SOME (y, xs') => rep (y :: ys) xs');
   in rep [] end;
 
-fun repeat1 scan = scan -- repeat scan >> op ::;
+fun repeat1 scan = scan ::: repeat scan;
 
 fun single scan = scan >> (fn x => [x]);
 fun bulk scan = scan -- repeat (permissive scan) >> (op ::);

--- a/src/Pure/Isar/args.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/Pure/Isar/args.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -288,10 +288,10 @@
 
 (* enumerations *)
 
-fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
+fun list1 scan = scan ::: Scan.repeat ($$$ "," |-- scan);
 fun list scan = list1 scan || Scan.succeed [];
 
-fun enum1 sep scan = scan -- Scan.repeat (Scan.lift ($$$ sep) |-- scan) >> op ::;
+fun enum1 sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
 fun enum sep scan = enum1 sep scan || Scan.succeed [];
 
 fun and_list1 scan = enum1 "and" scan;

--- a/src/Pure/Isar/class.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/Pure/Isar/class.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -763,7 +763,7 @@
       ((junk |--
         (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
         --| junk))
-      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
+      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
   in
     explode #> scan_valids #> implode
   end;

--- a/src/Pure/Isar/outer_parse.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -185,7 +185,7 @@
 
 (* enumerations *)
 
-fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- !!! scan) >> op ::;
+fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
 fun enum sep scan = enum1 sep scan || Scan.succeed [];
 
 fun list1 scan = enum1 "," scan;

--- a/src/Pure/Isar/spec_parse.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -108,7 +108,7 @@
     >> (curry Element.Notes "");
 
 fun plus1_unless test scan =
-  scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::;
+  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
 
 val rename = P.name -- Scan.option P.mixfix;
 

--- a/src/Pure/Syntax/simple_syntax.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -44,8 +44,8 @@
 (* basic scanners *)
 
 fun $$ s = Scan.some (fn Lexicon.Token s' => if s = s' then SOME s else NONE | _ => NONE);
-fun enum1 s scan = scan -- Scan.repeat ($$ s |-- scan) >> op ::;
-fun enum2 s scan = scan -- Scan.repeat1 ($$ s |-- scan) >> op ::;
+fun enum1 s scan = scan ::: Scan.repeat ($$ s |-- scan);
+fun enum2 s scan = scan ::: Scan.repeat1 ($$ s |-- scan);
 
 val tfree = Scan.some (fn Lexicon.TFreeSy s => SOME s | _ => NONE);
 val ident = Scan.some (fn Lexicon.IdentSy s => SOME s | _ => NONE);

--- a/src/Tools/code/code_name.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/Tools/code/code_name.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -49,7 +49,7 @@
       ((junk |--
         (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
         --| junk))
-      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
+      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
     fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
       else if lower then (if forall Symbol.is_ascii_upper cs
         then map else nth_map 0) Symbol.to_ascii_lower cs