get_index: produce index of next pending token, not the last one;

--- 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