# HG changeset patch
# User wenzelm
# Date 1237907469 -3600
# Node ID e8ab35c6ade6ff88d0aaaffc6c74975a0efb92f8
# Parent  d6d4828e74a269431b3640ff6934f4f0e778b209
get_index: produce index of next pending token, not the last one;

diff -r d6d4828e74a2 -r e8ab35c6ade6 src/Pure/ML/ml_test.ML
--- a/src/Pure/ML/ml_test.ML	Tue Mar 24 15:47:55 2009 +0100
+++ b/src/Pure/ML/ml_test.ML	Tue Mar 24 16:11:09 2009 +0100
@@ -69,7 +69,9 @@
 
     val current_line = ref (the_default 1 (Position.line_of pos));
 
-    fun get_index () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
+    fun get_index () =
+      the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
+
     fun get () =
       (case ! input_buffer of
         [] => NONE