| author | nipkow | 
| Wed, 13 Dec 2017 13:25:14 +0100 | |
| changeset 67170 | 9bfe79084443 | 
| parent 56782 | 433cf57550fa | 
| child 68806 | 4597812d5182 | 
| 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  | 
|
| 51980 | 24  | 
var debug = false  | 
25  | 
||
| 
48346
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
26  | 
def tool(body: => Int): Nothing =  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
27  | 
  {
 | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
28  | 
val rc =  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
29  | 
      try { body }
 | 
| 51980 | 30  | 
      catch {
 | 
31  | 
case exn: Throwable =>  | 
|
32  | 
if (debug) exn.printStackTrace  | 
|
| 
56782
 
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
 
wenzelm 
parents: 
56671 
diff
changeset
 | 
33  | 
Output.error_message(Exn.message(exn))  | 
| 
56669
 
f42717b5dc84
clarified message and return code, in accordance to ML version;
 
wenzelm 
parents: 
56631 
diff
changeset
 | 
34  | 
Exn.return_code(exn, 2)  | 
| 51980 | 35  | 
}  | 
| 
48346
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
36  | 
sys.exit(rc)  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
37  | 
}  | 
| 56631 | 38  | 
|
39  | 
  def tool0(body: => Unit): Nothing = tool { body; 0 }
 | 
|
| 
48346
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
40  | 
}  | 
| 
 
e2382bede914
more general support for Isabelle/Scala command line tools;
 
wenzelm 
parents:  
diff
changeset
 | 
41  |