1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/etc/options Fri Jul 20 21:05:47 2012 +0200
1.3 @@ -0,0 +1,24 @@
1.4 +(* :mode=isabelle-options: *)
1.5 +
1.6 +declare browser_info : bool = false
1.7 +
1.8 +declare document : bool = true
1.9 +declare document_format : string = pdf
1.10 +declare document_variants : string = document
1.11 +declare document_graph : bool = false
1.12 +
1.13 +declare threads_limit : int = 1
1.14 +declare threads_trace : int = 0
1.15 +declare parallel_proofs : int = 1
1.16 +declare parallel_proofs_threshold : int = 100
1.17 +
1.18 +declare print_mode : string = ""
1.19 +
1.20 +declare proofs : int = 0
1.21 +declare quick_and_dirty : bool = false
1.22 +
1.23 +declare timing : bool = false
1.24 +declare verbose : bool = false
1.25 +
1.26 +declare condition : string = ""
1.27 +
2.1 --- a/src/Pure/General/path.scala Fri Jul 20 10:53:25 2012 +0200
2.2 +++ b/src/Pure/General/path.scala Fri Jul 20 21:05:47 2012 +0200
2.3 @@ -8,6 +8,8 @@
2.4 package isabelle
2.5
2.6
2.7 +import java.io.File
2.8 +
2.9 import scala.util.matching.Regex
2.10
2.11
2.12 @@ -162,4 +164,9 @@
2.13
2.14 new Path(Path.norm_elems(elems.map(eval).flatten))
2.15 }
2.16 +
2.17 +
2.18 + /* platform file */
2.19 +
2.20 + def file: File = Isabelle_System.platform_file(this)
2.21 }
3.1 --- a/src/Pure/General/position.scala Fri Jul 20 10:53:25 2012 +0200
3.2 +++ b/src/Pure/General/position.scala Fri Jul 20 21:05:47 2012 +0200
3.3 @@ -17,6 +17,9 @@
3.4 val File = new Properties.String(Isabelle_Markup.FILE)
3.5 val Id = new Properties.Long(Isabelle_Markup.ID)
3.6
3.7 + def file(f: java.io.File): T = File(Isabelle_System.posix_path(f.toString))
3.8 + def line_file(i: Int, f: java.io.File): T = Line(i) ::: file(f)
3.9 +
3.10 object Range
3.11 {
3.12 def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
3.13 @@ -47,4 +50,13 @@
3.14 def purge(props: T): T =
3.15 for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
3.16 yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
3.17 +
3.18 +
3.19 + def str_of(props: T): String =
3.20 + (Line.unapply(props), File.unapply(props)) match {
3.21 + case (Some(i), None) => " (line " + i.toString + ")"
3.22 + case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
3.23 + case (None, Some(name)) => " (file " + quote(name) + ")"
3.24 + case _ => ""
3.25 + }
3.26 }
4.1 --- a/src/Pure/Isar/token.scala Fri Jul 20 10:53:25 2012 +0200
4.2 +++ b/src/Pure/Isar/token.scala Fri Jul 20 21:05:47 2012 +0200
4.3 @@ -73,8 +73,10 @@
4.4 kind == Token.Kind.ALT_STRING ||
4.5 kind == Token.Kind.VERBATIM ||
4.6 kind == Token.Kind.COMMENT
4.7 + def is_ident: Boolean = kind == Token.Kind.IDENT
4.8 def is_string: Boolean = kind == Token.Kind.STRING
4.9 def is_nat: Boolean = kind == Token.Kind.NAT
4.10 + def is_float: Boolean = kind == Token.Kind.FLOAT
4.11 def is_name: Boolean =
4.12 kind == Token.Kind.IDENT ||
4.13 kind == Token.Kind.SYM_IDENT ||
5.1 --- a/src/Pure/System/build.scala Fri Jul 20 10:53:25 2012 +0200
5.2 +++ b/src/Pure/System/build.scala Fri Jul 20 21:05:47 2012 +0200
5.3 @@ -75,6 +75,14 @@
5.4 new Queue(keys1, graph1)
5.5 }
5.6
5.7 + def required(names: List[String]): Queue =
5.8 + {
5.9 + val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
5.10 + val keys1 = keys -- keys.keySet.filter(name => !req(name))
5.11 + val graph1 = graph.restrict(key => keys1.isDefinedAt(key.name))
5.12 + new Queue(keys1, graph1)
5.13 + }
5.14 +
5.15 def topological_order: List[(Key, Info)] =
5.16 graph.topological_order.map(key => (key, graph.get_node(key)))
5.17 }
5.18 @@ -145,20 +153,25 @@
5.19
5.20 /* find sessions */
5.21
5.22 - private def sessions_root(dir: Path, root: File, sessions: Session.Queue): Session.Queue =
5.23 + private val ROOT = Path.explode("ROOT")
5.24 + private val SESSIONS = Path.explode("etc/sessions")
5.25 +
5.26 + private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
5.27 +
5.28 + private def sessions_root(dir: Path, root: File, queue: Session.Queue): Session.Queue =
5.29 {
5.30 - (sessions /: Parser.parse_entries(root))((sessions1, entry) =>
5.31 + (queue /: Parser.parse_entries(root))((queue1, entry) =>
5.32 try {
5.33 if (entry.name == "") error("Bad session name")
5.34
5.35 val full_name =
5.36 - if (entry.name == "RAW" || entry.name == "Pure") {
5.37 + if (is_pure(entry.name)) {
5.38 if (entry.parent.isDefined) error("Illegal parent session")
5.39 else entry.name
5.40 }
5.41 else
5.42 entry.parent match {
5.43 - case Some(parent_name) if sessions1.defined(parent_name) =>
5.44 + case Some(parent_name) if queue1.defined(parent_name) =>
5.45 if (entry.reset) entry.name
5.46 else parent_name + "-" + entry.name
5.47 case _ => error("Bad parent session")
5.48 @@ -174,32 +187,32 @@
5.49 val info = Session.Info(dir + path, entry.description, entry.options,
5.50 entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
5.51
5.52 - sessions1 + (key, info, entry.parent)
5.53 + queue1 + (key, info, entry.parent)
5.54 }
5.55 catch {
5.56 case ERROR(msg) =>
5.57 error(msg + "\nThe error(s) above occurred in session entry " +
5.58 - quote(entry.name) + " (file " + quote(root.toString) + ")")
5.59 + quote(entry.name) + Position.str_of(Position.file(root)))
5.60 })
5.61 }
5.62
5.63 - private def sessions_dir(strict: Boolean, dir: Path, sessions: Session.Queue): Session.Queue =
5.64 + private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
5.65 {
5.66 - val root = Isabelle_System.platform_file(dir + Path.basic("ROOT"))
5.67 - if (root.isFile) sessions_root(dir, root, sessions)
5.68 + val root = (dir + ROOT).file
5.69 + if (root.isFile) sessions_root(dir, root, queue)
5.70 else if (strict) error("Bad session root file: " + quote(root.toString))
5.71 - else sessions
5.72 + else queue
5.73 }
5.74
5.75 - private def sessions_catalog(dir: Path, catalog: File, sessions: Session.Queue): Session.Queue =
5.76 + private def sessions_catalog(dir: Path, catalog: File, queue: Session.Queue): Session.Queue =
5.77 {
5.78 val dirs =
5.79 split_lines(Standard_System.read_file(catalog)).
5.80 filterNot(line => line == "" || line.startsWith("#"))
5.81 - (sessions /: dirs)((sessions1, dir1) =>
5.82 + (queue /: dirs)((queue1, dir1) =>
5.83 try {
5.84 val dir2 = dir + Path.explode(dir1)
5.85 - if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, sessions1)
5.86 + if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1)
5.87 else error("Bad session directory: " + dir2.toString)
5.88 }
5.89 catch {
5.90 @@ -210,36 +223,101 @@
5.91
5.92 def find_sessions(more_dirs: List[Path]): Session.Queue =
5.93 {
5.94 - var sessions = Session.Queue.empty
5.95 + var queue = Session.Queue.empty
5.96
5.97 for (dir <- Isabelle_System.components()) {
5.98 - sessions = sessions_dir(false, dir, sessions)
5.99 + queue = sessions_dir(false, dir, queue)
5.100
5.101 - val catalog = Isabelle_System.platform_file(dir + Path.explode("etc/sessions"))
5.102 + val catalog = (dir + SESSIONS).file
5.103 if (catalog.isFile)
5.104 - sessions = sessions_catalog(dir, catalog, sessions)
5.105 + queue = sessions_catalog(dir, catalog, queue)
5.106 }
5.107
5.108 - for (dir <- more_dirs) sessions = sessions_dir(true, dir, sessions)
5.109 + for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
5.110
5.111 - sessions
5.112 + queue
5.113 }
5.114
5.115
5.116
5.117 /** build **/
5.118
5.119 + private def echo(msg: String) { java.lang.System.out.println(msg) }
5.120 + private def echo_n(msg: String) { java.lang.System.out.print(msg) }
5.121 +
5.122 + private def build_job(build_images: Boolean, // FIXME
5.123 + key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
5.124 + {
5.125 + val cwd = info.dir.file
5.126 + val script =
5.127 + if (is_pure(key.name)) "./build " + (if (build_images) "-b " else "") + key.name
5.128 + else """echo "Bad session" >&2; exit 2"""
5.129 + new Isabelle_System.Bash_Job(cwd, null, script)
5.130 + }
5.131 +
5.132 def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
5.133 more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
5.134 {
5.135 - println("more_dirs = " + more_dirs.toString)
5.136 - println("options = " + options.toString)
5.137 - println("sessions = " + sessions.toString)
5.138 + val full_queue = find_sessions(more_dirs)
5.139 + val build_options = (Options.init() /: options)(_.define_simple(_))
5.140
5.141 - for ((key, info) <- find_sessions(more_dirs).topological_order)
5.142 - println(key.name + " in " + info.dir)
5.143 + sessions.filter(name => !full_queue.defined(name)) match {
5.144 + case Nil =>
5.145 + case bad => error("Undefined session(s): " + commas_quote(bad))
5.146 + }
5.147
5.148 - 0
5.149 + val required_queue =
5.150 + if (all_sessions) full_queue
5.151 + else full_queue.required(sessions)
5.152 +
5.153 + // prepare browser info dir
5.154 + if (build_options.bool("browser_info") &&
5.155 + !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
5.156 + {
5.157 + Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
5.158 + Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file,
5.159 + Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file)
5.160 + Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file,
5.161 + Standard_System.read_file(
5.162 + Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) +
5.163 + Standard_System.read_file(
5.164 + Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) +
5.165 + Standard_System.read_file(
5.166 + Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file))
5.167 + }
5.168 +
5.169 + // prepare log dir
5.170 + val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
5.171 + log_dir.file.mkdirs()
5.172 +
5.173 + // run jobs
5.174 + val rcs =
5.175 + for ((key, info) <- required_queue.topological_order) yield
5.176 + {
5.177 + if (list_only) { echo(key.name + " in " + info.dir); 0 }
5.178 + else {
5.179 + if (build_images) echo("Building " + key.name + "...")
5.180 + else echo("Running " + key.name + "...")
5.181 +
5.182 + val (out, err, rc) = build_job(build_images, key, info).join
5.183 + echo_n(err)
5.184 +
5.185 + val log = log_dir + Path.basic(key.name)
5.186 + if (rc == 0) {
5.187 + Standard_System.write_file(log.ext("gz").file, out, true)
5.188 + }
5.189 + else {
5.190 + Standard_System.write_file(log.file, out)
5.191 + echo(key.name + " FAILED")
5.192 + echo("(see also " + log.file + ")")
5.193 + val lines = split_lines(out)
5.194 + val tail = lines.drop(lines.length - 20 max 0)
5.195 + echo("\n" + cat_lines(tail))
5.196 + }
5.197 + rc
5.198 + }
5.199 + }
5.200 + (0 /: rcs)(_ max _)
5.201 }
5.202
5.203
6.1 --- a/src/Pure/System/isabelle_system.scala Fri Jul 20 10:53:25 2012 +0200
6.2 +++ b/src/Pure/System/isabelle_system.scala Fri Jul 20 21:05:47 2012 +0200
6.3 @@ -146,10 +146,9 @@
6.4 if (path.is_absolute || path.is_current)
6.5 try_file(platform_file(path))
6.6 else {
6.7 - val pure_file = platform_file(Path.explode("~~/src/Pure") + path)
6.8 + val pure_file = (Path.explode("~~/src/Pure") + path).file
6.9 if (pure_file.isFile) Some(pure_file)
6.10 - else if (getenv("ML_SOURCES") != "")
6.11 - try_file(platform_file(Path.explode("$ML_SOURCES") + path))
6.12 + else if (getenv("ML_SOURCES") != "") try_file((Path.explode("$ML_SOURCES") + path).file)
6.13 else None
6.14 }
6.15 }
6.16 @@ -278,7 +277,7 @@
6.17 def isabelle_tool(name: String, args: String*): (String, Int) =
6.18 {
6.19 Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
6.20 - val file = platform_file(dir + Path.basic(name))
6.21 + val file = (dir + Path.basic(name)).file
6.22 try {
6.23 file.isFile && file.canRead && file.canExecute &&
6.24 !name.endsWith("~") && !name.endsWith(".orig")
6.25 @@ -309,7 +308,7 @@
6.26 val ml_ident = getenv_strict("ML_IDENTIFIER")
6.27 val logics = new mutable.ListBuffer[String]
6.28 for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
6.29 - val files = platform_file(dir + Path.explode(ml_ident)).listFiles()
6.30 + val files = (dir + Path.explode(ml_ident)).file.listFiles()
6.31 if (files != null) {
6.32 for (file <- files if file.isFile) logics += file.getName
6.33 }
6.34 @@ -327,6 +326,6 @@
6.35 {
6.36 val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
6.37 for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
6.38 - ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
6.39 + ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
6.40 }
6.41 }
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Pure/System/options.scala Fri Jul 20 21:05:47 2012 +0200
7.3 @@ -0,0 +1,205 @@
7.4 +/* Title: Pure/System/options.scala
7.5 + Author: Makarius
7.6 +
7.7 +Stand-alone options with external string representation.
7.8 +*/
7.9 +
7.10 +package isabelle
7.11 +
7.12 +
7.13 +import java.io.File
7.14 +
7.15 +
7.16 +object Options
7.17 +{
7.18 + abstract class Type
7.19 + {
7.20 + def print: String = toString.toLowerCase
7.21 + }
7.22 + case object Bool extends Type
7.23 + case object Int extends Type
7.24 + case object Real extends Type
7.25 + case object String extends Type
7.26 +
7.27 + case class Opt(typ: Type, value: String, description: String)
7.28 +
7.29 + val empty: Options = new Options()
7.30 +
7.31 +
7.32 + /* parsing */
7.33 +
7.34 + private object Parser extends Parse.Parser
7.35 + {
7.36 + val DECLARE = "declare"
7.37 + val DEFINE = "define"
7.38 +
7.39 + val syntax = Outer_Syntax.empty + ":" + "=" + DECLARE + DEFINE
7.40 +
7.41 + val entry: Parser[Options => Options] =
7.42 + {
7.43 + val option_name = atom("option name", _.is_xname)
7.44 + val option_type = atom("option type", _.is_ident)
7.45 + val option_value = atom("option value", tok => tok.is_name || tok.is_float)
7.46 +
7.47 + keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
7.48 + keyword("=") ~ option_value ~ opt(text)) ^^
7.49 + { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) =>
7.50 + (options: Options) => options.declare(a, b, c, d.getOrElse("")) } |
7.51 + keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
7.52 + { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
7.53 + }
7.54 +
7.55 + def parse_entries(file: File): List[Options => Options] =
7.56 + {
7.57 + val toks = syntax.scan(Standard_System.read_file(file))
7.58 + parse_all(rep(entry), Token.reader(toks, file.toString)) match {
7.59 + case Success(result, _) => result
7.60 + case bad => error(bad.toString)
7.61 + }
7.62 + }
7.63 + }
7.64 +
7.65 + val OPTIONS = Path.explode("etc/options")
7.66 +
7.67 + def init(): Options =
7.68 + {
7.69 + var options = empty
7.70 + for {
7.71 + dir <- Isabelle_System.components()
7.72 + file = (dir + OPTIONS).file
7.73 + if file.isFile
7.74 + entry <- Parser.parse_entries(file)
7.75 + } {
7.76 + try { options = entry(options) }
7.77 + catch { case ERROR(msg) => error(msg + Position.str_of(Position.file(file))) }
7.78 + }
7.79 + options
7.80 + }
7.81 +}
7.82 +
7.83 +
7.84 +final class Options private(options: Map[String, Options.Opt] = Map.empty)
7.85 +{
7.86 + override def toString: String = options.iterator.mkString("Options (", ",", ")")
7.87 +
7.88 +
7.89 + /* check */
7.90 +
7.91 + private def check_name(name: String): Options.Opt =
7.92 + options.get(name) match {
7.93 + case Some(opt) => opt
7.94 + case None => error("Unknown option " + quote(name))
7.95 + }
7.96 +
7.97 + private def check_type(name: String, typ: Options.Type): Options.Opt =
7.98 + {
7.99 + val opt = check_name(name)
7.100 + if (opt.typ == typ) opt
7.101 + else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
7.102 + }
7.103 +
7.104 +
7.105 + /* basic operations */
7.106 +
7.107 + private def put[A](name: String, typ: Options.Type, value: String): Options =
7.108 + {
7.109 + val opt = check_type(name, typ)
7.110 + new Options(options + (name -> opt.copy(value = value)))
7.111 + }
7.112 +
7.113 + private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
7.114 + {
7.115 + val opt = check_type(name, typ)
7.116 + parse(opt.value) match {
7.117 + case Some(x) => x
7.118 + case None =>
7.119 + error("Malformed value for option " + quote(name) +
7.120 + " : " + typ.print + " =\n" + quote(opt.value))
7.121 + }
7.122 + }
7.123 +
7.124 +
7.125 + /* internal lookup and update */
7.126 +
7.127 + val bool = new Object
7.128 + {
7.129 + def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
7.130 + def update(name: String, x: Boolean): Options =
7.131 + put(name, Options.Bool, Properties.Value.Boolean(x))
7.132 + }
7.133 +
7.134 + val int = new Object
7.135 + {
7.136 + def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
7.137 + def update(name: String, x: Int): Options =
7.138 + put(name, Options.Int, Properties.Value.Int(x))
7.139 + }
7.140 +
7.141 + val real = new Object
7.142 + {
7.143 + def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
7.144 + def update(name: String, x: Double): Options =
7.145 + put(name, Options.Real, Properties.Value.Double(x))
7.146 + }
7.147 +
7.148 + val string = new Object
7.149 + {
7.150 + def apply(name: String): String = get(name, Options.String, s => Some(s))
7.151 + def update(name: String, x: String): Options = put(name, Options.String, x)
7.152 + }
7.153 +
7.154 +
7.155 + /* external declare and define */
7.156 +
7.157 + private def check_value(name: String): Options =
7.158 + {
7.159 + val opt = check_name(name)
7.160 + opt.typ match {
7.161 + case Options.Bool => bool(name); this
7.162 + case Options.Int => int(name); this
7.163 + case Options.Real => real(name); this
7.164 + case Options.String => string(name); this
7.165 + }
7.166 + }
7.167 +
7.168 + def declare(name: String, typ_name: String, value: String, description: String = ""): Options =
7.169 + {
7.170 + options.get(name) match {
7.171 + case Some(_) => error("Duplicate declaration of option " + quote(name))
7.172 + case None =>
7.173 + val typ =
7.174 + typ_name match {
7.175 + case "bool" => Options.Bool
7.176 + case "int" => Options.Int
7.177 + case "real" => Options.Real
7.178 + case "string" => Options.String
7.179 + case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name))
7.180 + }
7.181 + (new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name)
7.182 + }
7.183 + }
7.184 +
7.185 + def define(name: String, value: String): Options =
7.186 + {
7.187 + val opt = check_name(name)
7.188 + (new Options(options + (name -> opt.copy(value = value)))).check_value(name)
7.189 + }
7.190 +
7.191 + def define(name: String, opt_value: Option[String]): Options =
7.192 + {
7.193 + val opt = check_name(name)
7.194 + opt_value match {
7.195 + case Some(value) => define(name, value)
7.196 + case None if opt.typ == Options.Bool => define(name, "true")
7.197 + case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
7.198 + }
7.199 + }
7.200 +
7.201 + def define_simple(str: String): Options =
7.202 + {
7.203 + str.indexOf('=') match {
7.204 + case -1 => define(str, None)
7.205 + case i => define(str.substring(0, i), str.substring(i + 1))
7.206 + }
7.207 + }
7.208 +}
8.1 --- a/src/Pure/System/standard_system.scala Fri Jul 20 10:53:25 2012 +0200
8.2 +++ b/src/Pure/System/standard_system.scala Fri Jul 20 21:05:47 2012 +0200
8.3 @@ -15,6 +15,7 @@
8.4 BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
8.5 File, FileFilter, IOException}
8.6 import java.nio.charset.Charset
8.7 +import java.util.zip.GZIPOutputStream
8.8
8.9 import scala.io.Codec
8.10 import scala.util.matching.Regex
8.11 @@ -115,14 +116,36 @@
8.12
8.13 def read_file(file: File): String = slurp(new FileInputStream(file))
8.14
8.15 - def write_file(file: File, text: CharSequence)
8.16 + def write_file(file: File, text: CharSequence, zip: Boolean = false)
8.17 {
8.18 - val writer =
8.19 - new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
8.20 + val stream1 = new FileOutputStream(file)
8.21 + val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
8.22 + val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
8.23 try { writer.append(text) }
8.24 finally { writer.close }
8.25 }
8.26
8.27 + def eq_file(file1: File, file2: File): Boolean =
8.28 + file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
8.29 +
8.30 + def copy_file(src: File, dst: File) =
8.31 + if (!eq_file(src, dst)) {
8.32 + val in = new FileInputStream(src)
8.33 + try {
8.34 + val out = new FileOutputStream(dst)
8.35 + try {
8.36 + val buf = new Array[Byte](65536)
8.37 + var m = 0
8.38 + do {
8.39 + m = in.read(buf, 0, buf.length)
8.40 + if (m != -1) out.write(buf, 0, m)
8.41 + } while (m != -1)
8.42 + }
8.43 + finally { out.close }
8.44 + }
8.45 + finally { in.close }
8.46 + }
8.47 +
8.48 def with_tmp_file[A](prefix: String)(body: File => A): A =
8.49 {
8.50 val file = File.createTempFile(prefix, null)
9.1 --- a/src/Pure/System/system_channel.scala Fri Jul 20 10:53:25 2012 +0200
9.2 +++ b/src/Pure/System/system_channel.scala Fri Jul 20 21:05:47 2012 +0200
9.3 @@ -47,8 +47,7 @@
9.4 }
9.5
9.6 private def rm_fifo(fifo: String): Boolean =
9.7 - Isabelle_System.platform_file(
9.8 - Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).delete
9.9 + Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo).file.delete
9.10
9.11 private def fifo_input_stream(fifo: String): InputStream =
9.12 {
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/Pure/build Fri Jul 20 21:05:47 2012 +0200
10.3 @@ -0,0 +1,114 @@
10.4 +#!/usr/bin/env bash
10.5 +#
10.6 +# Author: Makarius
10.7 +#
10.8 +# build - build Isabelle/ML
10.9 +#
10.10 +# Requires proper Isabelle settings environment.
10.11 +
10.12 +
10.13 +## diagnostics
10.14 +
10.15 +function usage()
10.16 +{
10.17 + echo
10.18 + echo "Usage: $PRG [OPTIONS] TARGET"
10.19 + echo
10.20 + echo " Options are:"
10.21 + echo " -b build target images"
10.22 + echo
10.23 + echo " Build Isabelle/ML TARGET: RAW or Pure"
10.24 + echo
10.25 + exit 1
10.26 +}
10.27 +
10.28 +function fail()
10.29 +{
10.30 + echo "$1" >&2
10.31 + exit 2
10.32 +}
10.33 +
10.34 +[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
10.35 +
10.36 +
10.37 +## process command line
10.38 +
10.39 +# options
10.40 +
10.41 +BUILD_IMAGES=false
10.42 +
10.43 +while getopts "b" OPT
10.44 +do
10.45 + case "$OPT" in
10.46 + b)
10.47 + BUILD_IMAGES="true"
10.48 + ;;
10.49 + \?)
10.50 + usage
10.51 + ;;
10.52 + esac
10.53 +done
10.54 +
10.55 +shift $(($OPTIND - 1))
10.56 +
10.57 +
10.58 +# args
10.59 +
10.60 +TARGET="Pure"
10.61 +[ "$#" -ge 1 ] && { TARGET="$1"; shift; }
10.62 +[ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""
10.63 +
10.64 +[ "$#" -eq 0 ] || usage
10.65 +
10.66 +
10.67 +## main
10.68 +
10.69 +# get compatibility file
10.70 +
10.71 +ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
10.72 +[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
10.73 +
10.74 +COMPAT=""
10.75 +[ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML"
10.76 +[ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML"
10.77 +[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
10.78 +
10.79 +
10.80 +# run isabelle
10.81 +
10.82 +. "$ISABELLE_HOME/lib/scripts/timestart.bash"
10.83 +
10.84 +if [ "$TARGET" = RAW ]; then
10.85 + if [ "$BUILD_IMAGES" = false ]; then
10.86 + "$ISABELLE_PROCESS" \
10.87 + -e "use\"$COMPAT\" handle _ => exit 1;" \
10.88 + -q RAW_ML_SYSTEM
10.89 + else
10.90 + "$ISABELLE_PROCESS" \
10.91 + -e "use\"$COMPAT\" handle _ => exit 1;" \
10.92 + -e "structure Isar = struct fun main () = () end;" \
10.93 + -e "ml_prompts \"ML> \" \"ML# \";" \
10.94 + -q -w RAW_ML_SYSTEM RAW
10.95 + fi
10.96 +else
10.97 + if [ "$BUILD_IMAGES" = false ]; then
10.98 + "$ISABELLE_PROCESS" \
10.99 + -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
10.100 + -q RAW_ML_SYSTEM
10.101 + else
10.102 + "$ISABELLE_PROCESS" \
10.103 + -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
10.104 + -e "ml_prompts \"ML> \" \"ML# \";" \
10.105 + -f -q -w RAW_ML_SYSTEM Pure
10.106 + fi
10.107 +fi
10.108 +
10.109 +RC="$?"
10.110 +
10.111 +. "$ISABELLE_HOME/lib/scripts/timestop.bash"
10.112 +
10.113 +if [ "$RC" -eq 0 ]; then
10.114 + echo "Finished $TARGET ($TIMES_REPORT)" >&2
10.115 +fi
10.116 +
10.117 +exit "$RC"
11.1 --- a/src/Pure/build-jars Fri Jul 20 10:53:25 2012 +0200
11.2 +++ b/src/Pure/build-jars Fri Jul 20 21:05:47 2012 +0200
11.3 @@ -48,6 +48,7 @@
11.4 System/isabelle_process.scala
11.5 System/isabelle_system.scala
11.6 System/main.scala
11.7 + System/options.scala
11.8 System/platform.scala
11.9 System/session.scala
11.10 System/session_manager.scala
12.1 --- a/src/Pure/library.scala Fri Jul 20 10:53:25 2012 +0200
12.2 +++ b/src/Pure/library.scala Fri Jul 20 21:05:47 2012 +0200
12.3 @@ -100,7 +100,7 @@
12.4
12.5 def quote(s: String): String = "\"" + s + "\""
12.6 def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
12.7 - def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
12.8 + def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
12.9
12.10
12.11 /* reverse CharSequence */
13.1 --- a/src/Tools/jEdit/lib/Tools/jedit Fri Jul 20 10:53:25 2012 +0200
13.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jul 20 21:05:47 2012 +0200
13.3 @@ -230,6 +230,7 @@
13.4 perl -i -e 'while (<>) {
13.5 if (m/NAME="javacc"/) {
13.6 print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
13.7 + print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;
13.8 print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
13.9 elsif (m/NAME="scheme"/) {
13.10 print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Tools/jEdit/src/modes/isabelle-options.xml Fri Jul 20 21:05:47 2012 +0200
14.3 @@ -0,0 +1,37 @@
14.4 +<?xml version="1.0"?>
14.5 +<!DOCTYPE MODE SYSTEM "xmode.dtd">
14.6 +
14.7 +<!-- Isabelle options mode -->
14.8 +<MODE>
14.9 + <PROPS>
14.10 + <PROPERTY NAME="commentStart" VALUE="(*"/>
14.11 + <PROPERTY NAME="commentEnd" VALUE="*)"/>
14.12 + <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
14.13 + <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
14.14 + <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
14.15 + <PROPERTY NAME="tabSize" VALUE="2" />
14.16 + <PROPERTY NAME="indentSize" VALUE="2" />
14.17 + </PROPS>
14.18 + <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
14.19 + <SPAN TYPE="COMMENT1">
14.20 + <BEGIN>(*</BEGIN>
14.21 + <END>*)</END>
14.22 + </SPAN>
14.23 + <SPAN TYPE="COMMENT3">
14.24 + <BEGIN>{*</BEGIN>
14.25 + <END>*}</END>
14.26 + </SPAN>
14.27 + <SPAN TYPE="LITERAL2">
14.28 + <BEGIN>`</BEGIN>
14.29 + <END>`</END>
14.30 + </SPAN>
14.31 + <SPAN TYPE="LITERAL1">
14.32 + <BEGIN>"</BEGIN>
14.33 + <END>"</END>
14.34 + </SPAN>
14.35 + <KEYWORDS>
14.36 + <KEYWORD1>declare</KEYWORD1>
14.37 + <KEYWORD2>define</KEYWORD2>
14.38 + </KEYWORDS>
14.39 + </RULES>
14.40 +</MODE>