# HG changeset patch # User wenzelm # Date 1175638274 -7200 # Node ID 4b1ecb19b411e542d65af9ce71e9091b218c5dd3 # Parent f315da9400fbe9afd94d7bc3325a0f5fd54a3e3c added scanwords from library.ML (for obsolete rename_tac); diff -r f315da9400fb -r 4b1ecb19b411 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Wed Apr 04 00:11:13 2007 +0200 +++ b/src/Pure/tactic.ML Wed Apr 04 00:11:14 2007 +0200 @@ -515,6 +515,15 @@ Logic.auto_rename := false) else (); PRIMITIVE (rename_params_rule (xs, i))); +(*scan a list of characters into "words" composed of "letters" (recognized by + is_let) and separated by any number of non-"letters"*) +fun scanwords is_let cs = + let fun scan1 [] = [] + | scan1 cs = + let val (lets, rest) = take_prefix is_let cs + in implode lets :: scanwords is_let rest end; + in scan1 (#2 (take_prefix (not o is_let) cs)) end; + fun rename_tac str i = let val cs = Symbol.explode str in case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of