# HG changeset patch
# User wenzelm
# Date 1087073199 -7200
# Node ID 66d797e1b950ac136be21f698e4e6509c258fbe5
# Parent  d2baf4b79424f6ea732f835085db5f8241ea243f
added trace (inefficient for very long input);

diff -r d2baf4b79424 -r 66d797e1b950 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sat Jun 12 22:46:21 2004 +0200
+++ b/src/Pure/General/scan.ML	Sat Jun 12 22:46:39 2004 +0200
@@ -30,9 +30,6 @@
   val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
   (*one element literal*)
   val $$ : ''a -> ''a list -> ''a * ''a list
-  (*literal list*)
-  val this: ''a list -> ''a list -> ''a list * ''a list
-  val this_string: string -> string list -> string * string list
 end;
 
 signature SCAN =
@@ -41,6 +38,8 @@
   val fail: 'a -> 'b
   val fail_with: ('a -> string) -> 'a -> 'b
   val succeed: 'a -> 'b -> 'a * 'b
+  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
@@ -52,6 +51,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 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 lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
@@ -203,6 +203,10 @@
 fun first [] = fail
   | first (scan :: scans) = scan || first scans;
 
+fun trace scan toks =
+  let val (x, toks') = scan toks
+  in ((x, take (length toks - length toks', toks)), toks') end;
+
 
 (* state based scanners *)