# HG changeset patch # User wenzelm # Date 1342811147 -7200 # Node ID 623607c5a40f1cf69dff83e05ce6fbdaa802a063 # Parent 868dc809c8a21ee59046d4082eb253dc46442bb2# Parent 527e2bad7cca004d5f153e002953f1b33f17b739 merged diff -r 868dc809c8a2 -r 623607c5a40f etc/options --- /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 = "" + diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/General/path.scala --- 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) } diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/General/position.scala --- 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 _ => "" + } } diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/Isar/token.scala --- 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 || diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/System/build.scala --- 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 _) } diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/System/isabelle_system.scala --- 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)) } } diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/System/options.scala --- /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)) + } + } +} diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/System/standard_system.scala --- 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) diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/System/system_channel.scala --- 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 = { diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/build --- /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" diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/build-jars --- 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 diff -r 868dc809c8a2 -r 623607c5a40f src/Pure/library.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 */ diff -r 868dc809c8a2 -r 623607c5a40f src/Tools/jEdit/lib/Tools/jedit --- 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,\n\n,; + print qq,\n\n,; print qq,\n\n,; } elsif (m/NAME="scheme"/) { print qq,\n\n,; } diff -r 868dc809c8a2 -r 623607c5a40f src/Tools/jEdit/src/modes/isabelle-options.xml --- /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 @@ + + + + + + + + + + + + + + + + + (* + *) + + + {* + *} + + + ` + ` + + + " + " + + + declare + define + + +