# HG changeset patch
# User wenzelm
# Date 1112858789 -7200
# Node ID 7c150afba112c2102238a421811fd56c8f8052ba
# Parent  6e6233e8cf5e84558c6e0c07a2587dbd05bbecc7
added some, peek, trace'; tuned;

diff -r 6e6233e8cf5e -r 7c150afba112 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Thu Apr 07 09:26:18 2005 +0200
+++ b/src/Pure/General/scan.ML	Thu Apr 07 09:26:29 2005 +0200
@@ -37,9 +37,10 @@
   val fail: 'a -> 'b
   val fail_with: ('a -> string) -> 'a -> 'b
   val succeed: 'a -> 'b -> 'a * 'b
+  val some: ('a -> 'b option) -> 'a list -> 'b * 'a list
+  val one: ('a -> bool) -> 'a list -> 'a * 'a list
   val this: ''a list -> ''a list -> ''a list * ''a list
   val this_string: string -> string list -> string * string list
-  val one: ('a -> bool) -> 'a list -> 'a * 'a list
   val any: ('a -> bool) -> 'a list -> 'a list * 'a list
   val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
   val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
@@ -50,11 +51,14 @@
   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 trace: ('a list -> 'b * 'c list) -> 'a list -> ('b * 'a list) * 'c list
   val state: 'a * 'b -> 'a * ('a * 'b)
   val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
+  val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd)
+  val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
   val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
-  val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
+  val trace': ('a * 'b list -> 'c * ('d * 'e list)) -> 'a * 'b list ->
+    ('c * 'b list) * ('d * 'e list)
+  val trace: ('a list -> 'b * 'c list) -> 'a list -> ('b * 'a list) * 'c list
   val try: ('a -> 'b) -> 'a -> 'b
   val force: ('a -> 'b) -> 'a -> 'b
   val prompt: string -> ('a -> 'b) -> 'a -> 'b
@@ -96,45 +100,45 @@
 (* scanner combinators *)
 
 (*dependent pairing*)
-fun (sc1 :-- sc2) toks =
+fun (scan1 :-- scan2) toks =
   let
-    val (x, toks2) = sc1 toks
-    val (y, toks3) = sc2 x toks2
+    val (x, toks2) = scan1 toks;
+    val (y, toks3) = scan2 x toks2;
   in ((x, y), toks3) end;
 
 (*sequential pairing*)
-fun (sc1 -- sc2) toks =
+fun (scan1 -- scan2) toks =
   let
-    val (x, toks2) = sc1 toks
-    val (y, toks3) = sc2 toks2
+    val (x, toks2) = scan1 toks;
+    val (y, toks3) = scan2 toks2;
   in ((x, y), toks3) end;
 
 (*application*)
-fun (sc >> f) toks =
-  let val (x, toks2) = sc toks
+fun (scan >> f) toks =
+  let val (x, toks2) = scan toks;
   in (f x, toks2) end;
 
 (*forget snd*)
-fun (sc1 --| sc2) toks =
+fun (scan1 --| scan2) toks =
   let
-    val (x, toks2) = sc1 toks
-    val (_, toks3) = sc2 toks2
+    val (x, toks2) = scan1 toks;
+    val (_, toks3) = scan2 toks2;
   in (x, toks3) end;
 
 (*forget fst*)
-fun (sc1 |-- sc2) toks =
-  let val (_, toks2) = sc1 toks
-  in sc2 toks2 end;
+fun (scan1 |-- scan2) toks =
+  let val (_, toks2) = scan1 toks;
+  in scan2 toks2 end;
 
 (*concatenation*)
-fun (sc1 ^^ sc2) toks =
+fun (scan1 ^^ scan2) toks =
   let
-    val (x, toks2) = sc1 toks
-    val (y, toks3) = sc2 toks2
+    val (x, toks2) = scan1 toks;
+    val (y, toks3) = scan2 toks2;
   in (x ^ y, toks3) end;
 
 (*alternative*)
-fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
+fun (scan1 || scan2) toks = scan1 toks handle FAIL _ => scan2 toks;
 
 
 (* generic scanners *)
@@ -143,6 +147,10 @@
 fun fail_with msg_of xs = raise FAIL (SOME (msg_of xs));
 fun succeed y xs = (y, xs);
 
+fun some _ [] = raise MORE NONE
+  | some f (x :: xs) =
+      (case f x of SOME y => (y, xs) | _ => raise FAIL NONE);
+
 fun one _ [] = raise MORE NONE
   | one pred (x :: xs) =
       if pred x then (x, xs) else raise FAIL NONE;
@@ -159,32 +167,27 @@
           if y = x then drop_prefix ys xs else raise FAIL NONE;
   in (ys, drop_prefix ys xs) end;
 
-fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols yet!*)
+fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)
 
 fun any _ [] = raise MORE NONE
   | any pred (lst as x :: xs) =
       if pred x then apfst (cons x) (any pred xs)
       else ([], lst);
 
-fun any1 p toks =
-  let
-    val (x, toks2) = one p toks
-    val (xs,toks3) = any p toks2
-  in (x :: xs, toks3) end;
+fun any1 pred = one pred -- any pred >> op ::;
 
-fun optional scan def =  scan || succeed def
-fun option scan = (scan >> SOME) || succeed NONE
+fun optional scan def = scan || succeed def;
+fun option scan = (scan >> SOME) || succeed NONE;
 
 fun repeat scan =
-  let fun rep ys xs = (case (SOME (scan xs) handle FAIL _ => NONE) of
-    NONE => (rev ys, xs) | SOME (y, xs') => rep (y :: ys) xs')
+  let
+    fun rep ys xs =
+      (case (SOME (scan xs) handle FAIL _ => NONE) of
+        NONE => (rev ys, xs)
+      | SOME (y, xs') => rep (y :: ys) xs');
   in rep [] end;
 
-fun repeat1 scan toks =
-  let
-    val (x, toks2) = scan toks
-    val (xs, toks3) = repeat scan toks2
-  in (x :: xs, toks3) end;
+fun repeat1 scan = scan -- repeat scan >> op ::;
 
 fun max leq scan1 scan2 xs =
   (case (option scan1 xs, option scan2 xs) of
@@ -202,10 +205,6 @@
 fun first [] = fail
   | first (scan :: scans) = scan || first scans;
 
-fun trace scan toks =
-  let val (x, toks') = scan toks
-  in ((x, Library.take (length toks - length toks', toks)), toks') end;
-
 
 (* state based scanners *)
 
@@ -215,13 +214,26 @@
   let val ((st', y), xs') = scan st xs
   in (y, (st', xs')) end;
 
+fun peek scan = depend (fn st => scan st >> pair st);
+
+fun pass st scan xs =
+  let val (y, (_, xs')) = scan (st, xs)
+  in (y, xs') end;
+
 fun lift scan (st, xs) =
   let val (y, xs') = scan xs
   in (y, (st, xs')) end;
 
-fun pass st scan xs =
-  let val (y, (_, xs')) = scan (st, xs)
-  in (y, xs') end;
+fun unlift scan = pass () scan;
+
+
+(* trace input *)
+
+fun trace' scan (st, xs) =
+  let val (y, (st', xs')) = scan (st, xs)
+  in ((y, Library.take (length xs - length xs', xs)), (st', xs')) end;
+
+fun trace scan = unlift (trace' (lift scan));
 
 
 (* exception handling *)
@@ -247,12 +259,10 @@
   in
     if exists is_stopper input then
       raise ABORT "Stopper may not occur in input of finite scan!"
-    else (force scan --| lift stop) (state, List.revAppend (rev input,[stopper]))
+    else (force scan --| lift stop) (state, List.revAppend (rev input, [stopper]))
   end;
 
-fun finite stopper scan xs =
-  let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
-  in (y, xs') end;
+fun finite stopper scan = unlift (finite' stopper (lift scan));
 
 fun read stopper scan xs =
   (case error (finite stopper (option scan)) xs of
@@ -264,7 +274,7 @@
 
 fun drain def_prmpt get stopper scan ((state, xs), src) =
   (scan (state, xs), src) handle MORE prmpt =>
-    (case get (getOpt (prmpt,def_prmpt)) src of
+    (case get (getOpt (prmpt, def_prmpt)) src of
       ([], _) => (finite' stopper scan (state, xs), src)
     | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
 
@@ -274,7 +284,7 @@
 
     fun drain_loop recover inp =
       drain_with (catch scanner) inp handle FAIL msg =>
-        (error_msg (getOpt (msg,"Syntax error.")); drain_with recover inp);
+        (error_msg (getOpt (msg, "Syntax error.")); drain_with recover inp);
 
     val ((ys, (state', xs')), src') =
       (case (get def_prmpt src, opt_recover) of
@@ -283,10 +293,8 @@
       | ((xs, s), SOME r) => drain_loop (unless (lift (one (#2 stopper))) r) ((state, xs), s));
   in (ys, (state', unget (xs', src'))) end;
 
-fun source def_prmpt get unget stopper scan opt_recover src =
-  let val (ys, ((), src')) =
-    source' def_prmpt get unget stopper (lift scan) (Option.map lift opt_recover) ((), src)
-  in (ys, src') end;
+fun source def_prmpt get unget stopper scan opt_recover =
+  unlift (source' def_prmpt get unget stopper (lift scan) (Option.map lift opt_recover));
 
 fun single scan = scan >> (fn x => [x]);
 fun bulk scan = scan -- repeat (try scan) >> (op ::);
diff -r 6e6233e8cf5e -r 7c150afba112 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Apr 07 09:26:18 2005 +0200
+++ b/src/Pure/codegen.ML	Thu Apr 07 09:26:29 2005 +0200
@@ -225,8 +225,8 @@
 fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
 
 val code_attr =
-  Attrib.syntax (Scan.depend (fn thy => foldr op || Scan.fail (map mk_parser
-    (#attrs (CodegenData.get thy))) >> pair thy));
+  Attrib.syntax (Scan.peek (fn thy => foldr op || Scan.fail (map mk_parser
+    (#attrs (CodegenData.get thy)))));
 
 
 (**** preprocessors ****)