Lines Matching refs:get_token
319 fun parse_definition get_token (tydict, tmdict, proof) =
321 val _ = Library.expect_token "(" (get_token ())
322 val _ = Library.expect_token "(" (get_token ())
323 val name = get_token ()
324 val t = SmtLib_Parser.parse_term get_token (tydict, tmdict)
325 val _ = Library.expect_token ")" (get_token ())
326 val _ = Library.expect_token ")" (get_token ())
344 fun parse_proof get_token (tydict, tmdict, proof) (rpars : int) =
346 val _ = Library.expect_token "(" (get_token ())
347 val head = get_token ()
351 val (tmdict, proof) = parse_definition get_token (tydict, tmdict, proof)
353 parse_proof get_token (tydict, tmdict, proof) (rpars + 1)
358 get_token ();
359 Library.expect_token ")" (get_token ());
360 parse_proof get_token (tydict, tmdict, proof) rpars
365 fun get_token' () =
367 [] => get_token ()
369 val t = SmtLib_Parser.parse_term get_token' (tydict, tmdict)
373 (fn () => Library.expect_token ")" (get_token ())) ()
392 val get_token = Library.get_token (Library.get_buffered_char instream)
393 val proof = parse_proof get_token
396 WARNING "parse_stream" ("ignoring token '" ^ get_token () ^