src/Pure/ML/ml_test.ML
changeset 30705 e8ab35c6ade6
parent 30704 d6d4828e74a2
child 30709 d9ca766bf24c
equal deleted inserted replaced
30704:d6d4828e74a2 30705:e8ab35c6ade6
    67     val input = Context.>>> (register_tokens toks);
    67     val input = Context.>>> (register_tokens toks);
    68     val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
    68     val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
    69 
    69 
    70     val current_line = ref (the_default 1 (Position.line_of pos));
    70     val current_line = ref (the_default 1 (Position.line_of pos));
    71 
    71 
    72     fun get_index () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
    72     fun get_index () =
       
    73       the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
       
    74 
    73     fun get () =
    75     fun get () =
    74       (case ! input_buffer of
    76       (case ! input_buffer of
    75         [] => NONE
    77         [] => NONE
    76       | (_, []) :: rest => (input_buffer := rest; get ())
    78       | (_, []) :: rest => (input_buffer := rest; get ())
    77       | (i, c :: cs) :: rest =>
    79       | (i, c :: cs) :: rest =>