src/Pure/General/scan.scala
changeset 59319 677615cba30d
parent 59073 dcecfcc56dce
child 60215 5fb4990dfc73
equal deleted inserted replaced
59318:3ef6b0b6232e 59319:677615cba30d
   328       val len = str.length
   328       val len = str.length
   329       @tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
   329       @tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] =
   330       {
   330       {
   331         if (i < len) {
   331         if (i < len) {
   332           tree.branches.get(str.charAt(i)) match {
   332           tree.branches.get(str.charAt(i)) match {
   333             case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
   333             case Some((s, tr)) => look(tr, s.nonEmpty, i + 1)
   334             case None => None
   334             case None => None
   335           }
   335           }
   336         }
   336         }
   337         else Some(tip, tree)
   337         else Some(tip, tree)
   338       }
   338       }