--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/etc/options Fri Jul 20 21:05:47 2012 +0200
@@ -0,0 +1,24 @@
+(* :mode=isabelle-options: *)
+
+declare browser_info : bool = false
+
+declare document : bool = true
+declare document_format : string = pdf
+declare document_variants : string = document
+declare document_graph : bool = false
+
+declare threads_limit : int = 1
+declare threads_trace : int = 0
+declare parallel_proofs : int = 1
+declare parallel_proofs_threshold : int = 100
+
+declare print_mode : string = ""
+
+declare proofs : int = 0
+declare quick_and_dirty : bool = false
+
+declare timing : bool = false
+declare verbose : bool = false
+
+declare condition : string = ""
+
--- a/src/Pure/General/path.scala Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Pure/General/path.scala Fri Jul 20 21:05:47 2012 +0200
@@ -8,6 +8,8 @@
package isabelle
+import java.io.File
+
import scala.util.matching.Regex
@@ -162,4 +164,9 @@
new Path(Path.norm_elems(elems.map(eval).flatten))
}
+
+
+ /* platform file */
+
+ def file: File = Isabelle_System.platform_file(this)
}
--- a/src/Pure/General/position.scala Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Pure/General/position.scala Fri Jul 20 21:05:47 2012 +0200
@@ -17,6 +17,9 @@
val File = new Properties.String(Isabelle_Markup.FILE)
val Id = new Properties.Long(Isabelle_Markup.ID)
+ def file(f: java.io.File): T = File(Isabelle_System.posix_path(f.toString))
+ def line_file(i: Int, f: java.io.File): T = Line(i) ::: file(f)
+
object Range
{
def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
@@ -47,4 +50,13 @@
def purge(props: T): T =
for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
+
+
+ def str_of(props: T): String =
+ (Line.unapply(props), File.unapply(props)) match {
+ case (Some(i), None) => " (line " + i.toString + ")"
+ case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
+ case (None, Some(name)) => " (file " + quote(name) + ")"
+ case _ => ""
+ }
}
--- a/src/Pure/Isar/token.scala Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Pure/Isar/token.scala Fri Jul 20 21:05:47 2012 +0200
@@ -73,8 +73,10 @@
kind == Token.Kind.ALT_STRING ||
kind == Token.Kind.VERBATIM ||
kind == Token.Kind.COMMENT
+ def is_ident: Boolean = kind == Token.Kind.IDENT
def is_string: Boolean = kind == Token.Kind.STRING
def is_nat: Boolean = kind == Token.Kind.NAT
+ def is_float: Boolean = kind == Token.Kind.FLOAT
def is_name: Boolean =
kind == Token.Kind.IDENT ||
kind == Token.Kind.SYM_IDENT ||
--- a/src/Pure/System/build.scala Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Pure/System/build.scala Fri Jul 20 21:05:47 2012 +0200
@@ -75,6 +75,14 @@
new Queue(keys1, graph1)
}
+ def required(names: List[String]): Queue =
+ {
+ val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
+ val keys1 = keys -- keys.keySet.filter(name => !req(name))
+ val graph1 = graph.restrict(key => keys1.isDefinedAt(key.name))
+ new Queue(keys1, graph1)
+ }
+
def topological_order: List[(Key, Info)] =
graph.topological_order.map(key => (key, graph.get_node(key)))
}
@@ -145,20 +153,25 @@
/* find sessions */
- private def sessions_root(dir: Path, root: File, sessions: Session.Queue): Session.Queue =
+ private val ROOT = Path.explode("ROOT")
+ private val SESSIONS = Path.explode("etc/sessions")
+
+ private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
+
+ private def sessions_root(dir: Path, root: File, queue: Session.Queue): Session.Queue =
{
- (sessions /: Parser.parse_entries(root))((sessions1, entry) =>
+ (queue /: Parser.parse_entries(root))((queue1, entry) =>
try {
if (entry.name == "") error("Bad session name")
val full_name =
- if (entry.name == "RAW" || entry.name == "Pure") {
+ if (is_pure(entry.name)) {
if (entry.parent.isDefined) error("Illegal parent session")
else entry.name
}
else
entry.parent match {
- case Some(parent_name) if sessions1.defined(parent_name) =>
+ case Some(parent_name) if queue1.defined(parent_name) =>
if (entry.reset) entry.name
else parent_name + "-" + entry.name
case _ => error("Bad parent session")
@@ -174,32 +187,32 @@
val info = Session.Info(dir + path, entry.description, entry.options,
entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
- sessions1 + (key, info, entry.parent)
+ queue1 + (key, info, entry.parent)
}
catch {
case ERROR(msg) =>
error(msg + "\nThe error(s) above occurred in session entry " +
- quote(entry.name) + " (file " + quote(root.toString) + ")")
+ quote(entry.name) + Position.str_of(Position.file(root)))
})
}
- private def sessions_dir(strict: Boolean, dir: Path, sessions: Session.Queue): Session.Queue =
+ private def sessions_dir(strict: Boolean, dir: Path, queue: Session.Queue): Session.Queue =
{
- val root = Isabelle_System.platform_file(dir + Path.basic("ROOT"))
- if (root.isFile) sessions_root(dir, root, sessions)
+ val root = (dir + ROOT).file
+ if (root.isFile) sessions_root(dir, root, queue)
else if (strict) error("Bad session root file: " + quote(root.toString))
- else sessions
+ else queue
}
- private def sessions_catalog(dir: Path, catalog: File, sessions: Session.Queue): Session.Queue =
+ private def sessions_catalog(dir: Path, catalog: File, queue: Session.Queue): Session.Queue =
{
val dirs =
split_lines(Standard_System.read_file(catalog)).
filterNot(line => line == "" || line.startsWith("#"))
- (sessions /: dirs)((sessions1, dir1) =>
+ (queue /: dirs)((queue1, dir1) =>
try {
val dir2 = dir + Path.explode(dir1)
- if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, sessions1)
+ if (dir2.file.isDirectory) sessions_dir(true, dir2, queue1)
else error("Bad session directory: " + dir2.toString)
}
catch {
@@ -210,36 +223,101 @@
def find_sessions(more_dirs: List[Path]): Session.Queue =
{
- var sessions = Session.Queue.empty
+ var queue = Session.Queue.empty
for (dir <- Isabelle_System.components()) {
- sessions = sessions_dir(false, dir, sessions)
+ queue = sessions_dir(false, dir, queue)
- val catalog = Isabelle_System.platform_file(dir + Path.explode("etc/sessions"))
+ val catalog = (dir + SESSIONS).file
if (catalog.isFile)
- sessions = sessions_catalog(dir, catalog, sessions)
+ queue = sessions_catalog(dir, catalog, queue)
}
- for (dir <- more_dirs) sessions = sessions_dir(true, dir, sessions)
+ for (dir <- more_dirs) queue = sessions_dir(true, dir, queue)
- sessions
+ queue
}
/** build **/
+ private def echo(msg: String) { java.lang.System.out.println(msg) }
+ private def echo_n(msg: String) { java.lang.System.out.print(msg) }
+
+ private def build_job(build_images: Boolean, // FIXME
+ key: Session.Key, info: Session.Info): Isabelle_System.Bash_Job =
+ {
+ val cwd = info.dir.file
+ val script =
+ if (is_pure(key.name)) "./build " + (if (build_images) "-b " else "") + key.name
+ else """echo "Bad session" >&2; exit 2"""
+ new Isabelle_System.Bash_Job(cwd, null, script)
+ }
+
def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
{
- println("more_dirs = " + more_dirs.toString)
- println("options = " + options.toString)
- println("sessions = " + sessions.toString)
+ val full_queue = find_sessions(more_dirs)
+ val build_options = (Options.init() /: options)(_.define_simple(_))
+
+ sessions.filter(name => !full_queue.defined(name)) match {
+ case Nil =>
+ case bad => error("Undefined session(s): " + commas_quote(bad))
+ }
+
+ val required_queue =
+ if (all_sessions) full_queue
+ else full_queue.required(sessions)
+
+ // prepare browser info dir
+ if (build_options.bool("browser_info") &&
+ !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
+ {
+ Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
+ Standard_System.copy_file(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif").file,
+ Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif").file)
+ Standard_System.write_file(Path.explode("$ISABELLE_BROWSER_INFO/index.html").file,
+ Standard_System.read_file(
+ Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template").file) +
+ Standard_System.read_file(
+ Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template").file) +
+ Standard_System.read_file(
+ Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template").file))
+ }
- for ((key, info) <- find_sessions(more_dirs).topological_order)
- println(key.name + " in " + info.dir)
+ // prepare log dir
+ val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
+ log_dir.file.mkdirs()
+
+ // run jobs
+ val rcs =
+ for ((key, info) <- required_queue.topological_order) yield
+ {
+ if (list_only) { echo(key.name + " in " + info.dir); 0 }
+ else {
+ if (build_images) echo("Building " + key.name + "...")
+ else echo("Running " + key.name + "...")
+
+ val (out, err, rc) = build_job(build_images, key, info).join
+ echo_n(err)
- 0
+ val log = log_dir + Path.basic(key.name)
+ if (rc == 0) {
+ Standard_System.write_file(log.ext("gz").file, out, true)
+ }
+ else {
+ Standard_System.write_file(log.file, out)
+ echo(key.name + " FAILED")
+ echo("(see also " + log.file + ")")
+ val lines = split_lines(out)
+ val tail = lines.drop(lines.length - 20 max 0)
+ echo("\n" + cat_lines(tail))
+ }
+ rc
+ }
+ }
+ (0 /: rcs)(_ max _)
}
--- a/src/Pure/System/isabelle_system.scala Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala Fri Jul 20 21:05:47 2012 +0200
@@ -146,10 +146,9 @@
if (path.is_absolute || path.is_current)
try_file(platform_file(path))
else {
- val pure_file = platform_file(Path.explode("~~/src/Pure") + path)
+ val pure_file = (Path.explode("~~/src/Pure") + path).file
if (pure_file.isFile) Some(pure_file)
- else if (getenv("ML_SOURCES") != "")
- try_file(platform_file(Path.explode("$ML_SOURCES") + path))
+ else if (getenv("ML_SOURCES") != "") try_file((Path.explode("$ML_SOURCES") + path).file)
else None
}
}
@@ -278,7 +277,7 @@
def isabelle_tool(name: String, args: String*): (String, Int) =
{
Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
- val file = platform_file(dir + Path.basic(name))
+ val file = (dir + Path.basic(name)).file
try {
file.isFile && file.canRead && file.canExecute &&
!name.endsWith("~") && !name.endsWith(".orig")
@@ -309,7 +308,7 @@
val ml_ident = getenv_strict("ML_IDENTIFIER")
val logics = new mutable.ListBuffer[String]
for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
- val files = platform_file(dir + Path.explode(ml_ident)).listFiles()
+ val files = (dir + Path.explode(ml_ident)).file.listFiles()
if (files != null) {
for (file <- files if file.isFile) logics += file.getName
}
@@ -327,6 +326,6 @@
{
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
- ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, platform_file(font)))
+ ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/options.scala Fri Jul 20 21:05:47 2012 +0200
@@ -0,0 +1,205 @@
+/* Title: Pure/System/options.scala
+ Author: Makarius
+
+Stand-alone options with external string representation.
+*/
+
+package isabelle
+
+
+import java.io.File
+
+
+object Options
+{
+ abstract class Type
+ {
+ def print: String = toString.toLowerCase
+ }
+ case object Bool extends Type
+ case object Int extends Type
+ case object Real extends Type
+ case object String extends Type
+
+ case class Opt(typ: Type, value: String, description: String)
+
+ val empty: Options = new Options()
+
+
+ /* parsing */
+
+ private object Parser extends Parse.Parser
+ {
+ val DECLARE = "declare"
+ val DEFINE = "define"
+
+ val syntax = Outer_Syntax.empty + ":" + "=" + DECLARE + DEFINE
+
+ val entry: Parser[Options => Options] =
+ {
+ val option_name = atom("option name", _.is_xname)
+ val option_type = atom("option type", _.is_ident)
+ val option_value = atom("option value", tok => tok.is_name || tok.is_float)
+
+ keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
+ keyword("=") ~ option_value ~ opt(text)) ^^
+ { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) =>
+ (options: Options) => options.declare(a, b, c, d.getOrElse("")) } |
+ keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
+ { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
+ }
+
+ def parse_entries(file: File): List[Options => Options] =
+ {
+ val toks = syntax.scan(Standard_System.read_file(file))
+ parse_all(rep(entry), Token.reader(toks, file.toString)) match {
+ case Success(result, _) => result
+ case bad => error(bad.toString)
+ }
+ }
+ }
+
+ val OPTIONS = Path.explode("etc/options")
+
+ def init(): Options =
+ {
+ var options = empty
+ for {
+ dir <- Isabelle_System.components()
+ file = (dir + OPTIONS).file
+ if file.isFile
+ entry <- Parser.parse_entries(file)
+ } {
+ try { options = entry(options) }
+ catch { case ERROR(msg) => error(msg + Position.str_of(Position.file(file))) }
+ }
+ options
+ }
+}
+
+
+final class Options private(options: Map[String, Options.Opt] = Map.empty)
+{
+ override def toString: String = options.iterator.mkString("Options (", ",", ")")
+
+
+ /* check */
+
+ private def check_name(name: String): Options.Opt =
+ options.get(name) match {
+ case Some(opt) => opt
+ case None => error("Unknown option " + quote(name))
+ }
+
+ private def check_type(name: String, typ: Options.Type): Options.Opt =
+ {
+ val opt = check_name(name)
+ if (opt.typ == typ) opt
+ else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
+ }
+
+
+ /* basic operations */
+
+ private def put[A](name: String, typ: Options.Type, value: String): Options =
+ {
+ val opt = check_type(name, typ)
+ new Options(options + (name -> opt.copy(value = value)))
+ }
+
+ private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A =
+ {
+ val opt = check_type(name, typ)
+ parse(opt.value) match {
+ case Some(x) => x
+ case None =>
+ error("Malformed value for option " + quote(name) +
+ " : " + typ.print + " =\n" + quote(opt.value))
+ }
+ }
+
+
+ /* internal lookup and update */
+
+ val bool = new Object
+ {
+ def apply(name: String): Boolean = get(name, Options.Bool, Properties.Value.Boolean.unapply)
+ def update(name: String, x: Boolean): Options =
+ put(name, Options.Bool, Properties.Value.Boolean(x))
+ }
+
+ val int = new Object
+ {
+ def apply(name: String): Int = get(name, Options.Int, Properties.Value.Int.unapply)
+ def update(name: String, x: Int): Options =
+ put(name, Options.Int, Properties.Value.Int(x))
+ }
+
+ val real = new Object
+ {
+ def apply(name: String): Double = get(name, Options.Real, Properties.Value.Double.unapply)
+ def update(name: String, x: Double): Options =
+ put(name, Options.Real, Properties.Value.Double(x))
+ }
+
+ val string = new Object
+ {
+ def apply(name: String): String = get(name, Options.String, s => Some(s))
+ def update(name: String, x: String): Options = put(name, Options.String, x)
+ }
+
+
+ /* external declare and define */
+
+ private def check_value(name: String): Options =
+ {
+ val opt = check_name(name)
+ opt.typ match {
+ case Options.Bool => bool(name); this
+ case Options.Int => int(name); this
+ case Options.Real => real(name); this
+ case Options.String => string(name); this
+ }
+ }
+
+ def declare(name: String, typ_name: String, value: String, description: String = ""): Options =
+ {
+ options.get(name) match {
+ case Some(_) => error("Duplicate declaration of option " + quote(name))
+ case None =>
+ val typ =
+ typ_name match {
+ case "bool" => Options.Bool
+ case "int" => Options.Int
+ case "real" => Options.Real
+ case "string" => Options.String
+ case _ => error("Malformed type for option " + quote(name) + " : " + quote(typ_name))
+ }
+ (new Options(options + (name -> Options.Opt(typ, value, description)))).check_value(name)
+ }
+ }
+
+ def define(name: String, value: String): Options =
+ {
+ val opt = check_name(name)
+ (new Options(options + (name -> opt.copy(value = value)))).check_value(name)
+ }
+
+ def define(name: String, opt_value: Option[String]): Options =
+ {
+ val opt = check_name(name)
+ opt_value match {
+ case Some(value) => define(name, value)
+ case None if opt.typ == Options.Bool => define(name, "true")
+ case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
+ }
+ }
+
+ def define_simple(str: String): Options =
+ {
+ str.indexOf('=') match {
+ case -1 => define(str, None)
+ case i => define(str.substring(0, i), str.substring(i + 1))
+ }
+ }
+}
--- a/src/Pure/System/standard_system.scala Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Pure/System/standard_system.scala Fri Jul 20 21:05:47 2012 +0200
@@ -15,6 +15,7 @@
BufferedInputStream, InputStream, FileInputStream, BufferedReader, InputStreamReader,
File, FileFilter, IOException}
import java.nio.charset.Charset
+import java.util.zip.GZIPOutputStream
import scala.io.Codec
import scala.util.matching.Regex
@@ -115,14 +116,36 @@
def read_file(file: File): String = slurp(new FileInputStream(file))
- def write_file(file: File, text: CharSequence)
+ def write_file(file: File, text: CharSequence, zip: Boolean = false)
{
- val writer =
- new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset))
+ val stream1 = new FileOutputStream(file)
+ val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
+ val writer = new BufferedWriter(new OutputStreamWriter(stream2, charset))
try { writer.append(text) }
finally { writer.close }
}
+ def eq_file(file1: File, file2: File): Boolean =
+ file1.getCanonicalPath == file2.getCanonicalPath // FIXME prefer java.nio.file.Files.isSameFile of Java 1.7
+
+ def copy_file(src: File, dst: File) =
+ if (!eq_file(src, dst)) {
+ val in = new FileInputStream(src)
+ try {
+ val out = new FileOutputStream(dst)
+ try {
+ val buf = new Array[Byte](65536)
+ var m = 0
+ do {
+ m = in.read(buf, 0, buf.length)
+ if (m != -1) out.write(buf, 0, m)
+ } while (m != -1)
+ }
+ finally { out.close }
+ }
+ finally { in.close }
+ }
+
def with_tmp_file[A](prefix: String)(body: File => A): A =
{
val file = File.createTempFile(prefix, null)
--- a/src/Pure/System/system_channel.scala Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Pure/System/system_channel.scala Fri Jul 20 21:05:47 2012 +0200
@@ -47,8 +47,7 @@
}
private def rm_fifo(fifo: String): Boolean =
- Isabelle_System.platform_file(
- Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo)).delete
+ Path.explode(if (Platform.is_windows) fifo + ".lnk" else fifo).file.delete
private def fifo_input_stream(fifo: String): InputStream =
{
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/build Fri Jul 20 21:05:47 2012 +0200
@@ -0,0 +1,114 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# build - build Isabelle/ML
+#
+# Requires proper Isabelle settings environment.
+
+
+## diagnostics
+
+function usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS] TARGET"
+ echo
+ echo " Options are:"
+ echo " -b build target images"
+ echo
+ echo " Build Isabelle/ML TARGET: RAW or Pure"
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
+
+
+## process command line
+
+# options
+
+BUILD_IMAGES=false
+
+while getopts "b" OPT
+do
+ case "$OPT" in
+ b)
+ BUILD_IMAGES="true"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+TARGET="Pure"
+[ "$#" -ge 1 ] && { TARGET="$1"; shift; }
+[ "$TARGET" = RAW -o "$TARGET" = Pure ] || fail "Bad target: \"$TARGET\""
+
+[ "$#" -eq 0 ] || usage
+
+
+## main
+
+# get compatibility file
+
+ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
+[ -z "$ML_SYSTEM" ] && fail "Missing ML_SYSTEM settings!"
+
+COMPAT=""
+[ -f "ML-Systems/${ML_SYSTEM_BASE}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM_BASE}.ML"
+[ -f "ML-Systems/${ML_SYSTEM}.ML" ] && COMPAT="ML-Systems/${ML_SYSTEM}.ML"
+[ -z "$COMPAT" ] && fail "Missing compatibility file for ML system \"$ML_SYSTEM\"!"
+
+
+# run isabelle
+
+. "$ISABELLE_HOME/lib/scripts/timestart.bash"
+
+if [ "$TARGET" = RAW ]; then
+ if [ "$BUILD_IMAGES" = false ]; then
+ "$ISABELLE_PROCESS" \
+ -e "use\"$COMPAT\" handle _ => exit 1;" \
+ -q RAW_ML_SYSTEM
+ else
+ "$ISABELLE_PROCESS" \
+ -e "use\"$COMPAT\" handle _ => exit 1;" \
+ -e "structure Isar = struct fun main () = () end;" \
+ -e "ml_prompts \"ML> \" \"ML# \";" \
+ -q -w RAW_ML_SYSTEM RAW
+ fi
+else
+ if [ "$BUILD_IMAGES" = false ]; then
+ "$ISABELLE_PROCESS" \
+ -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
+ -q RAW_ML_SYSTEM
+ else
+ "$ISABELLE_PROCESS" \
+ -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
+ -e "ml_prompts \"ML> \" \"ML# \";" \
+ -f -q -w RAW_ML_SYSTEM Pure
+ fi
+fi
+
+RC="$?"
+
+. "$ISABELLE_HOME/lib/scripts/timestop.bash"
+
+if [ "$RC" -eq 0 ]; then
+ echo "Finished $TARGET ($TIMES_REPORT)" >&2
+fi
+
+exit "$RC"
--- a/src/Pure/build-jars Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Pure/build-jars Fri Jul 20 21:05:47 2012 +0200
@@ -48,6 +48,7 @@
System/isabelle_process.scala
System/isabelle_system.scala
System/main.scala
+ System/options.scala
System/platform.scala
System/session.scala
System/session_manager.scala
--- a/src/Pure/library.scala Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Pure/library.scala Fri Jul 20 21:05:47 2012 +0200
@@ -100,7 +100,7 @@
def quote(s: String): String = "\"" + s + "\""
def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
- def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
+ def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
/* reverse CharSequence */
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Jul 20 10:53:25 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jul 20 21:05:47 2012 +0200
@@ -230,6 +230,7 @@
perl -i -e 'while (<>) {
if (m/NAME="javacc"/) {
print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
+ print qq,<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n,;
print qq,<MODE NAME="isabelle-session" FILE="isabelle-session.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
elsif (m/NAME="scheme"/) {
print qq,<MODE NAME="scala" FILE="scala.xml" FILE_NAME_GLOB="*.scala" />\n\n,; }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml Fri Jul 20 21:05:47 2012 +0200
@@ -0,0 +1,37 @@
+<?xml version="1.0"?>
+<!DOCTYPE MODE SYSTEM "xmode.dtd">
+
+<!-- Isabelle options mode -->
+<MODE>
+ <PROPS>
+ <PROPERTY NAME="commentStart" VALUE="(*"/>
+ <PROPERTY NAME="commentEnd" VALUE="*)"/>
+ <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
+ <PROPERTY NAME="tabSize" VALUE="2" />
+ <PROPERTY NAME="indentSize" VALUE="2" />
+ </PROPS>
+ <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
+ <SPAN TYPE="COMMENT1">
+ <BEGIN>(*</BEGIN>
+ <END>*)</END>
+ </SPAN>
+ <SPAN TYPE="COMMENT3">
+ <BEGIN>{*</BEGIN>
+ <END>*}</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL2">
+ <BEGIN>`</BEGIN>
+ <END>`</END>
+ </SPAN>
+ <SPAN TYPE="LITERAL1">
+ <BEGIN>"</BEGIN>
+ <END>"</END>
+ </SPAN>
+ <KEYWORDS>
+ <KEYWORD1>declare</KEYWORD1>
+ <KEYWORD2>define</KEYWORD2>
+ </KEYWORDS>
+ </RULES>
+</MODE>