| author | wenzelm | 
| Sun, 02 Sep 2012 19:26:05 +0200 | |
| changeset 49065 | 8ead9e8b15fb | 
| parent 48346 | e2382bede914 | 
| child 51980 | fe16d1128a14 | 
| permissions | -rw-r--r-- | 
| 
48346
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
1  | 
/* Title: Pure/System/command_line.scala  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
2  | 
Author: Makarius  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
3  | 
|
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
4  | 
Support for Isabelle/Scala command line tools.  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
5  | 
*/  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
6  | 
|
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
7  | 
package isabelle  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
8  | 
|
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
9  | 
|
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
10  | 
object Command_Line  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
11  | 
{
 | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
12  | 
object Chunks  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
13  | 
  {
 | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
14  | 
private def chunks(list: List[String]): List[List[String]] =  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
15  | 
      list.indexWhere(_ == "\n") match {
 | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
16  | 
case -1 => List(list)  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
17  | 
case i =>  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
18  | 
val (chunk, rest) = list.splitAt(i)  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
19  | 
chunk :: chunks(rest.tail)  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
20  | 
}  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
21  | 
def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
22  | 
}  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
23  | 
|
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
24  | 
def tool(body: => Int): Nothing =  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
25  | 
  {
 | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
26  | 
val rc =  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
27  | 
      try { body }
 | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
28  | 
      catch { case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 }
 | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
29  | 
sys.exit(rc)  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
30  | 
}  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
31  | 
}  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
32  |