# HG changeset patch
# User wenzelm
# Date 1082984309 -7200
# Node ID 33a37f091dc50bff36d2ca040c5a49a22ef89100
# Parent  82721f31de3ef565e22d961f4c61580b6e8e5223
tuned presentation;

diff -r 82721f31de3e -r 33a37f091dc5 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Mon Apr 26 14:58:03 2004 +0200
+++ b/src/Pure/General/scan.ML	Mon Apr 26 14:58:29 2004 +0200
@@ -12,23 +12,23 @@
 
 signature BASIC_SCAN =
 sig
-  (* error msg handler *)
+  (*error msg handler*)
   val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
-  (* apply function *)
+  (*apply function*)
   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
-  (* alternative *)
+  (*alternative*)
   val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
-  (* sequential pairing *)
+  (*sequential pairing*)
   val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
-  (* dependent pairing *)
+  (*dependent pairing*)
   val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
-  (* forget fst *)
+  (*forget fst*)
   val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
-  (* forget snd *)                                
+  (*forget snd*)
   val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
-  (* concatenation *)
+  (*concatenation*)
   val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
-  (* one element literal *)
+  (*one element literal*)
   val $$ : ''a -> ''a list -> ''a * ''a list
 end;
 
@@ -49,7 +49,7 @@
   val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
   val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
   val first: ('a -> 'b) list -> 'a -> 'b
-  val state: 'a * 'b -> 'a * ('a * 'b) 
+  val state: 'a * 'b -> 'a * ('a * 'b)
   val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
   val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
   val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
@@ -92,52 +92,45 @@
 
 (* scanner combinators *)
 
-(* dependent pairing *)
-
+(*dependent pairing*)
 fun (sc1 :-- sc2) toks =
   let
     val (x, toks2) = sc1 toks
     val (y, toks3) = sc2 x toks2
   in ((x, y), toks3) end;
 
-(* sequential pairing *)
-
+(*sequential pairing*)
 fun (sc1 -- sc2) toks =
   let
     val (x, toks2) = sc1 toks
     val (y, toks3) = sc2 toks2
   in ((x, y), toks3) end;
 
-(* application *)
-
+(*application*)
 fun (sc >> f) toks =
   let val (x, toks2) = sc toks
   in (f x, toks2) end;
 
-(* forget snd *)
-
+(*forget snd*)
 fun (sc1 --| sc2) toks =
   let
     val (x, toks2) = sc1 toks
     val (_, toks3) = sc2 toks2
   in (x, toks3) end;
 
-(* forget fst *)
-
+(*forget fst*)
 fun (sc1 |-- sc2) toks =
   let val (_, toks2) = sc1 toks
   in sc2 toks2 end;
 
-(* concatenation *)
-
+(*concatenation*)
 fun (sc1 ^^ sc2) toks =
   let
     val (x, toks2) = sc1 toks
     val (y, toks3) = sc2 toks2
   in (x ^ y, toks3) end;
 
-(* alternative *)
-
+(*alternative*)
 fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;