src/Pure/Tools/keywords.scala
changeset 56631 89269bb8e7ca
parent 56146 8453d35e4684
child 56830 e760242101fc
equal deleted inserted replaced
56630:d06c44532706 56631:89269bb8e7ca
   162 
   162 
   163   /* command line entry point */
   163   /* command line entry point */
   164 
   164 
   165   def main(args: Array[String])
   165   def main(args: Array[String])
   166   {
   166   {
   167     Command_Line.tool {
   167     Command_Line.tool0 {
   168       args.toList match {
   168       args.toList match {
   169         case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) =>
   169         case "keywords" :: name :: Command_Line.Chunks(dirs, sessions) =>
   170           keywords(Options.init(), name, dirs.map(Path.explode), sessions)
   170           keywords(Options.init(), name, dirs.map(Path.explode), sessions)
   171           0
       
   172         case "update_keywords" :: Nil =>
   171         case "update_keywords" :: Nil =>
   173           update_keywords(Options.init())
   172           update_keywords(Options.init())
   174           0
       
   175         case _ => error("Bad arguments:\n" + cat_lines(args))
   173         case _ => error("Bad arguments:\n" + cat_lines(args))
   176       }
   174       }
   177     }
   175     }
   178   }
   176   }
   179 }
   177 }