--- a/src/Pure/Admin/remote_dmg.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/Admin/remote_dmg.scala Tue Mar 13 19:35:08 2018 +0100
@@ -56,7 +56,7 @@
case _ => getopts.usage()
}
- val options = Options.init
+ val options = Options.init()
using(SSH.open_session(options, host = host, user = user, port = port))(
remote_dmg(_, tar_gz_file, dmg_file, volume_name))
}
--- a/src/Pure/GUI/gui.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/GUI/gui.scala Tue Mar 13 19:35:08 2018 +0100
@@ -7,7 +7,6 @@
package isabelle
import java.lang.{ClassLoader, ClassNotFoundException, NoSuchMethodException}
-import java.io.{FileInputStream, BufferedInputStream}
import java.awt.{GraphicsEnvironment, Image, Component, Container, Toolkit, Window, Font,
KeyboardFocusManager}
import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
--- a/src/Pure/General/json.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/General/json.scala Tue Mar 13 19:35:08 2018 +0100
@@ -17,8 +17,18 @@
type T = Any
type S = String
- type Object = Map[String, T]
- val empty: Object = Map.empty
+ object Object
+ {
+ type T = Map[String, JSON.T]
+ val empty: T = Map.empty
+
+ def unapply(obj: T): Option[Object.T] =
+ obj match {
+ case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
+ Some(m.asInstanceOf[Object.T])
+ case _ => None
+ }
+ }
/* lexer */
@@ -120,7 +130,7 @@
def string: Parser[String] = elem("string", _.is_string) ^^ (_.text)
def number: Parser[Double] = elem("number", _.is_number) ^^ (tok => tok.text.toDouble)
- def json_object: Parser[Object] =
+ def json_object: Parser[Object.T] =
$$$("{") ~>
repsep(string ~ ($$$(":") ~> json_value) ^^ { case a ~ b => (a, b) }, $$$(",")) <~
$$$("}") ^^ (_.toMap)
@@ -188,7 +198,7 @@
result += ']'
}
- def object_(obj: Object)
+ def object_(obj: Object.T)
{
result += '{'
Library.separate(None, obj.toList.map(Some(_))).foreach({
@@ -210,8 +220,7 @@
val i = n.toLong
result ++= (if (i.toDouble == n) i.toString else n.toString)
case s: String => string(s)
- case obj: Map[_, _] if obj.keySet.forall(_.isInstanceOf[String]) =>
- object_(obj.asInstanceOf[Object])
+ case Object(m) => object_(m)
case list: List[T] => array(list)
case _ => error("Bad JSON value: " + x.toString)
}
@@ -223,10 +232,18 @@
}
- /* numbers */
+ /* typed values */
- object Number
+ object Value
{
+ object String {
+ def unapply(json: T): Option[java.lang.String] =
+ json match {
+ case x: java.lang.String => Some(x)
+ case _ => None
+ }
+ }
+
object Double {
def unapply(json: T): Option[scala.Double] =
json match {
@@ -256,21 +273,39 @@
case _ => None
}
}
+
+ object Boolean {
+ def unapply(json: T): Option[scala.Boolean] =
+ json match {
+ case x: scala.Boolean => Some(x)
+ case _ => None
+ }
+ }
+
+ object List
+ {
+ def unapply[A](json: T, unapply: T => Option[A]): Option[List[A]] =
+ json match {
+ case xs: List[T] =>
+ val ys = xs.map(unapply)
+ if (ys.forall(_.isDefined)) Some(ys.map(_.get)) else None
+ case _ => None
+ }
+ }
}
/* object values */
- def optional(entry: (String, Option[T])): Object =
+ def optional(entry: (String, Option[T])): Object.T =
entry match {
case (name, Some(x)) => Map(name -> x)
- case (_, None) => empty
+ case (_, None) => Object.empty
}
def value(obj: T, name: String): Option[T] =
obj match {
- case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
- m.asInstanceOf[Object].get(name)
+ case Object(m) => m.get(name)
case _ => None
}
@@ -286,31 +321,39 @@
case _ => None
}
- def array[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] =
- for {
- a0 <- array(obj, name)
- a = a0.map(unapply(_))
- if a.forall(_.isDefined)
- } yield a.map(_.get)
+ def value_default[A](obj: T, name: String, unapply: T => Option[A], default: A): Option[A] =
+ value(obj, name) match {
+ case None => Some(default)
+ case Some(json) => unapply(json)
+ }
def string(obj: T, name: String): Option[String] =
- value(obj, name) match {
- case Some(x: String) => Some(x)
- case _ => None
- }
+ value(obj, name, Value.String.unapply)
+ def string_default(obj: T, name: String, default: String = ""): Option[String] =
+ value_default(obj, name, Value.String.unapply, default)
def double(obj: T, name: String): Option[Double] =
- value(obj, name, Number.Double.unapply)
+ value(obj, name, Value.Double.unapply)
+ def double_default(obj: T, name: String, default: Double = 0.0): Option[Double] =
+ value_default(obj, name, Value.Double.unapply, default)
def long(obj: T, name: String): Option[Long] =
- value(obj, name, Number.Long.unapply)
+ value(obj, name, Value.Long.unapply)
+ def long_default(obj: T, name: String, default: Long = 0): Option[Long] =
+ value_default(obj, name, Value.Long.unapply, default)
def int(obj: T, name: String): Option[Int] =
- value(obj, name, Number.Int.unapply)
+ value(obj, name, Value.Int.unapply)
+ def int_default(obj: T, name: String, default: Int = 0): Option[Int] =
+ value_default(obj, name, Value.Int.unapply, default)
def bool(obj: T, name: String): Option[Boolean] =
- value(obj, name) match {
- case Some(x: Boolean) => Some(x)
- case _ => None
- }
+ value(obj, name, Value.Boolean.unapply)
+ def bool_default(obj: T, name: String, default: Boolean = false): Option[Boolean] =
+ value_default(obj, name, Value.Boolean.unapply, default)
+
+ def list[A](obj: T, name: String, unapply: T => Option[A]): Option[List[A]] =
+ value(obj, name, Value.List.unapply(_, unapply))
+ def list_default[A](obj: T, name: String, unapply: T => Option[A], default: List[A] = Nil)
+ : Option[List[A]] = value_default(obj, name, Value.List.unapply(_, unapply), default)
}
--- a/src/Pure/ML/ml_console.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/ML/ml_console.scala Tue Mar 13 19:35:08 2018 +0100
@@ -52,14 +52,14 @@
// build
if (!no_build && !raw_ml_system &&
- !Build.build(options = options, build_heap = true, no_build = true,
+ !Build.build(options, build_heap = true, no_build = true,
dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
{
val progress = new Console_Progress()
progress.echo("Build started for Isabelle/" + logic + " ...")
progress.interrupt_handler {
val res =
- Build.build(options = options, progress = progress, build_heap = true,
+ Build.build(options, progress = progress, build_heap = true,
dirs = dirs, system_mode = system_mode, sessions = List(logic))
if (!res.ok) sys.exit(res.rc)
}
--- a/src/Pure/PIDE/markup.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/PIDE/markup.scala Tue Mar 13 19:35:08 2018 +0100
@@ -457,6 +457,7 @@
val STDOUT = "stdout"
val STDERR = "stderr"
val EXIT = "exit"
+ val LOGGER = "logger"
val WRITELN_MESSAGE = "writeln_message"
val STATE_MESSAGE = "state_message"
--- a/src/Pure/PIDE/prover.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/PIDE/prover.scala Tue Mar 13 19:35:08 2018 +0100
@@ -8,7 +8,7 @@
package isabelle
-import java.io.{InputStream, OutputStream, BufferedReader, BufferedOutputStream, IOException}
+import java.io.{InputStream, OutputStream, BufferedOutputStream, IOException}
object Prover
--- a/src/Pure/System/isabelle_system.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Mar 13 19:35:08 2018 +0100
@@ -8,7 +8,7 @@
package isabelle
-import java.io.{File => JFile, IOException, BufferedReader, InputStreamReader}
+import java.io.{File => JFile, IOException}
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
import java.nio.file.attribute.BasicFileAttributes
--- a/src/Pure/System/options.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/System/options.scala Tue Mar 13 19:35:08 2018 +0100
@@ -68,8 +68,7 @@
private val PUBLIC = "public"
private val OPTION = "option"
private val OPTIONS = Path.explode("etc/options")
- private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc")
- private val PREFS = PREFS_DIR + Path.basic("preferences")
+ private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences")
val options_syntax =
Outer_Syntax.empty + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
@@ -110,35 +109,37 @@
{ case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
}
- def parse_file(syntax: Outer_Syntax, parser: Parser[Options => Options],
- options: Options, file: Path): Options =
+ def parse_file(options: Options, file_name: String, content: String,
+ syntax: Outer_Syntax = options_syntax,
+ parser: Parser[Options => Options] = option_entry): Options =
{
- val toks = Token.explode(syntax.keywords, File.read(file))
+ val toks = Token.explode(syntax.keywords, content)
val ops =
- parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file.implode))) match {
+ parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file_name))) match {
case Success(result, _) => result
case bad => error(bad.toString)
}
try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } }
- catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
+ catch { case ERROR(msg) => error(msg + Position.File(file_name)) }
}
+
+ def parse_prefs(options: Options, content: String): Options =
+ parse_file(options, PREFS.base_name, content, syntax = prefs_syntax, parser = prefs_entry)
}
- def load(file: Path): Options =
- Parser.parse_file(options_syntax, Parser.option_entry, empty, file)
+ def read_prefs(file: Path = PREFS): String =
+ if (file.is_file) File.read(file) else ""
- def init_defaults(): Options =
+ def init(prefs: String = read_prefs(PREFS), opts: List[String] = Nil): Options =
{
var options = empty
for {
dir <- Isabelle_System.components()
file = dir + OPTIONS if file.is_file
- } { options = Parser.parse_file(options_syntax, Parser.option_entry, options, file) }
- options
+ } { options = Parser.parse_file(options, file.implode, File.read(file)) }
+ (Options.Parser.parse_prefs(options, prefs) /: opts)(_ + _)
}
- def init(): Options = init_defaults().load_prefs()
-
/* encode */
@@ -387,17 +388,11 @@
}
- /* user preferences */
+ /* save preferences */
- def load_prefs(): Options =
- if (Options.PREFS.is_file)
- Options.Parser.parse_file(
- Options.prefs_syntax, Options.Parser.prefs_entry, this, Options.PREFS)
- else this
-
- def save_prefs()
+ def save_prefs(file: Path = Options.PREFS)
{
- val defaults = Options.init_defaults()
+ val defaults: Options = Options.init(prefs = "")
val changed =
(for {
(name, opt2) <- options.iterator
@@ -409,8 +404,8 @@
changed.sortBy(_._1)
.map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
- Isabelle_System.mkdirs(Options.PREFS_DIR)
- File.write_backup(Options.PREFS, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs)
+ Isabelle_System.mkdirs(file.dir)
+ File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs)
}
}
--- a/src/Pure/System/tty_loop.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/System/tty_loop.scala Tue Mar 13 19:35:08 2018 +0100
@@ -7,13 +7,12 @@
package isabelle
-import java.io.{IOException, BufferedReader, BufferedWriter, InputStreamReader}
+import java.io.{IOException, Writer, Reader, InputStreamReader, BufferedReader}
-class TTY_Loop(
- process_writer: BufferedWriter,
- process_reader: BufferedReader,
- process_interrupt: Option[() => Unit] = None)
+class TTY_Loop(writer: Writer, reader: Reader,
+ writer_lock: AnyRef = new Object,
+ interrupt: Option[() => Unit] = None)
{
private val console_output = Future.thread[Unit]("console_output") {
try {
@@ -22,8 +21,8 @@
while (!finished) {
var c = -1
var done = false
- while (!done && (result.length == 0 || process_reader.ready)) {
- c = process_reader.read
+ while (!done && (result.length == 0 || reader.ready)) {
+ c = reader.read
if (c >= 0) result.append(c.asInstanceOf[Char])
else done = true
}
@@ -33,7 +32,7 @@
result.length = 0
}
else {
- process_reader.close()
+ reader.close()
finished = true
}
}
@@ -50,21 +49,22 @@
while (!finished) {
console_reader.readLine() match {
case null =>
- process_writer.close()
+ writer.close()
finished = true
case line =>
- process_writer.write(line)
- process_writer.write("\n")
- process_writer.flush()
+ writer_lock.synchronized {
+ writer.write(line)
+ writer.write("\n")
+ writer.flush()
+ }
}
}
}
catch { case e: IOException => case Exn.Interrupt() => }
}
- process_interrupt match {
+ interrupt match {
case None => body
- case Some(interrupt) =>
- POSIX_Interrupt.handler { interrupt() } { body }
+ case Some(int) => POSIX_Interrupt.handler { int() } { body }
}
}
--- a/src/Pure/Thy/sessions.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Mar 13 19:35:08 2018 +0100
@@ -367,7 +367,8 @@
def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
}
- def base_info(options: Options, session: String,
+ def base_info(options: Options,
+ session: String,
dirs: List[Path] = Nil,
ancestor_session: Option[String] = None,
all_known: Boolean = false,
--- a/src/Pure/Tools/build.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/Tools/build.scala Tue Mar 13 19:35:08 2018 +0100
@@ -8,12 +8,7 @@
package isabelle
-import java.io.{BufferedInputStream, FileInputStream,
- BufferedReader, InputStreamReader, IOException}
-import java.util.zip.GZIPInputStream
-
import scala.collection.SortedSet
-import scala.collection.mutable
import scala.annotation.tailrec
@@ -704,7 +699,7 @@
var check_keywords: Set[String] = Set.empty
var list_files = false
var no_build = false
- var options = (Options.init() /: build_options)(_ + _)
+ var options = Options.init(opts = build_options)
var system_mode = false
var verbose = false
var exclude_sessions: List[String] = Nil
@@ -775,7 +770,8 @@
val results =
progress.interrupt_handler {
- build(options, progress,
+ build(options,
+ progress = progress,
check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
build_heap = build_heap,
clean_build = clean_build,
--- a/src/Pure/Tools/server.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/Tools/server.scala Tue Mar 13 19:35:08 2018 +0100
@@ -19,8 +19,8 @@
package isabelle
-import java.io.{BufferedInputStream, BufferedOutputStream, BufferedReader, BufferedWriter,
- InputStreamReader, OutputStreamWriter, IOException}
+import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter,
+ IOException}
import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
@@ -32,7 +32,8 @@
{
def split(msg: String): (String, String) =
{
- val name = msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c))
+ val name =
+ msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c) || c == '.')
val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
(name, argument)
}
@@ -59,13 +60,17 @@
object Command
{
- type T = PartialFunction[(Server, Any), Any]
+ type T = PartialFunction[(Context, Any), Any]
private val table: Map[String, T] =
Map(
+ "help" -> { case (_, ()) => table.keySet.toList.sorted },
"echo" -> { case (_, t) => t },
- "help" -> { case (_, ()) => table.keySet.toList.sorted },
- "shutdown" -> { case (server, ()) => server.close(); () })
+ "shutdown" -> { case (context, ()) => context.shutdown(); () },
+ "session_build" ->
+ { case (context, Server_Commands.Session_Build(args)) =>
+ Server_Commands.Session_Build.command(context.progress(), args)._1
+ })
def unapply(name: String): Option[T] = table.get(name)
}
@@ -101,14 +106,24 @@
new Connection(socket)
}
- class Connection private(val socket: Socket)
+ class Connection private(socket: Socket)
{
override def toString: String = socket.toString
def close() { socket.close }
- val in = new BufferedInputStream(socket.getInputStream)
- val out = new BufferedOutputStream(socket.getOutputStream)
+ def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) }
+
+ private val in = new BufferedInputStream(socket.getInputStream)
+ private val out = new BufferedOutputStream(socket.getOutputStream)
+ private val out_lock: AnyRef = new Object
+
+ def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
+ new TTY_Loop(
+ new OutputStreamWriter(out),
+ new InputStreamReader(in),
+ writer_lock = out_lock,
+ interrupt = interrupt)
def read_message(): Option[String] =
try {
@@ -120,7 +135,7 @@
}
catch { case _: SocketException => None }
- def write_message(msg: String)
+ def write_message(msg: String): Unit = out_lock.synchronized
{
val b = UTF8.bytes(msg)
if (b.length > 100 || b.contains(10)) {
@@ -144,8 +159,51 @@
reply_error(Map("message" -> message) ++ more)
def notify(arg: Any) { reply(Server.Reply.NOTE, arg) }
- def notify_message(message: String, more: (String, JSON.T)*): Unit =
- notify(Map("message" -> message) ++ more)
+ }
+
+
+ /* context with output channels */
+
+ class Context private[Server](server: Server, connection: Connection)
+ {
+ context =>
+
+ def shutdown() { server.close() }
+
+ def notify(arg: Any) { connection.notify(arg) }
+ def message(kind: String, msg: String, more: (String, JSON.T)*): Unit =
+ notify(Map(Markup.KIND -> kind, "message" -> msg) ++ more)
+ def writeln(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WRITELN, msg, more:_*)
+ def warning(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WARNING, msg, more:_*)
+ def error_message(msg: String, more: (String, JSON.T)*): Unit =
+ message(Markup.ERROR_MESSAGE, msg, more:_*)
+
+ val logger: Connection_Logger = new Connection_Logger(context)
+ def progress(): Connection_Progress = new Connection_Progress(context)
+
+ override def toString: String = connection.toString
+ }
+
+ class Connection_Logger private[Server](context: Context) extends Logger
+ {
+ def apply(msg: => String): Unit = context.message(Markup.LOGGER, msg)
+
+ override def toString: String = context.toString
+ }
+
+ class Connection_Progress private[Server](context: Context) extends Progress
+ {
+ override def echo(msg: String): Unit = context.writeln(msg)
+ override def echo_warning(msg: String): Unit = context.warning(msg)
+ override def echo_error_message(msg: String): Unit = context.error_message(msg)
+ override def theory(session: String, theory: String): Unit =
+ context.writeln(session + ": theory " + theory, "session" -> session, "theory" -> theory)
+
+ @volatile private var is_stopped = false
+ override def stopped: Boolean = is_stopped
+ def stop { is_stopped = true }
+
+ override def toString: String = context.toString
}
@@ -167,7 +225,7 @@
try {
using(connection())(connection =>
{
- connection.socket.setSoTimeout(2000)
+ connection.set_timeout(Time.seconds(2.0))
connection.read_message() == Some(Reply.OK.toString)
})
}
@@ -176,18 +234,6 @@
case _: SocketException => false
case _: SocketTimeoutException => false
}
-
- def console()
- {
- using(connection())(connection =>
- {
- val tty_loop =
- new TTY_Loop(
- new BufferedWriter(new OutputStreamWriter(connection.socket.getOutputStream)),
- new BufferedReader(new InputStreamReader(connection.socket.getInputStream)))
- tty_loop.join
- })
- }
}
@@ -323,7 +369,9 @@
else {
val (server_info, server) = init(name, port = port, existing_server = existing_server)
Output.writeln(server_info.toString, stdout = true)
- if (console) server_info.console()
+ if (console) {
+ using(server_info.connection())(connection => connection.tty_loop().join)
+ }
server.foreach(_.join)
}
})
@@ -344,6 +392,8 @@
private def handle(connection: Server.Connection)
{
+ val context = new Server.Context(server, connection)
+
connection.read_message() match {
case Some(msg) if msg == password =>
connection.reply_ok(())
@@ -351,16 +401,15 @@
while (!finished) {
connection.read_message() match {
case None => finished = true
- case Some("") =>
- connection.notify_message("Command 'help' provides list of commands")
+ case Some("") => context.notify("Command 'help' provides list of commands")
case Some(msg) =>
val (name, argument) = Server.Argument.split(msg)
name match {
case Server.Command(cmd) =>
argument match {
case Server.Argument(arg) =>
- if (cmd.isDefinedAt((server, arg))) {
- Exn.capture { cmd((server, arg)) } match {
+ if (cmd.isDefinedAt((context, arg))) {
+ Exn.capture { cmd((context, arg)) } match {
case Exn.Res(res) => connection.reply_ok(res)
case Exn.Exn(ERROR(msg)) => connection.reply_error(msg)
case Exn.Exn(exn) => throw exn
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/server_commands.scala Tue Mar 13 19:35:08 2018 +0100
@@ -0,0 +1,70 @@
+/* Title: Pure/Tools/server_commands.scala
+ Author: Makarius
+
+Miscellaneous Isabelle server commands.
+*/
+
+package isabelle
+
+
+object Server_Commands
+{
+ object Session_Build
+ {
+ sealed case class Args(
+ session: String,
+ prefs: String = "",
+ opts: List[String] = Nil,
+ dirs: List[String] = Nil,
+ ancestor_session: String = "",
+ all_known: Boolean = false,
+ focus_session: Boolean = false,
+ required_session: Boolean = false,
+ system_mode: Boolean = false)
+
+ def unapply(json: JSON.T): Option[Args] =
+ for {
+ session <- JSON.string(json, "session")
+ prefs <- JSON.string_default(json, "preferences")
+ opts <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
+ dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
+ ancestor_session <- JSON.string_default(json, "ancestor_session")
+ all_known <- JSON.bool_default(json, "all_known")
+ focus_session <- JSON.bool_default(json, "focus_session")
+ required_session <- JSON.bool_default(json, "required_session")
+ system_mode <- JSON.bool_default(json, "system_mode")
+ }
+ yield {
+ Args(session, prefs = prefs, opts = opts, dirs = dirs, ancestor_session = ancestor_session,
+ all_known = all_known, focus_session = focus_session, required_session = required_session,
+ system_mode = system_mode)
+ }
+
+ def command(progress: Progress, args: Args): (JSON.T, Sessions.Base_Info, Build.Results) =
+ {
+ val options = Options.init(prefs = args.prefs, opts = args.opts)
+ val dirs = args.dirs.map(Path.explode(_))
+
+ val base_info =
+ Sessions.base_info(options,
+ args.session,
+ dirs = dirs,
+ ancestor_session = proper_string(args.ancestor_session),
+ all_known = args.all_known,
+ focus_session = args.focus_session,
+ required_session = args.required_session)
+ val base = base_info.check_base
+
+ val results =
+ Build.build(options,
+ progress = progress,
+ build_heap = true,
+ system_mode = args.system_mode,
+ dirs = dirs,
+ infos = base_info.infos,
+ sessions = List(args.session))
+
+ (Map("rc" -> results.rc), base_info, results)
+ }
+ }
+}
--- a/src/Pure/build-jars Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Pure/build-jars Tue Mar 13 19:35:08 2018 +0100
@@ -147,6 +147,7 @@
Tools/print_operation.scala
Tools/profiling_report.scala
Tools/server.scala
+ Tools/server_commands.scala
Tools/simplifier_trace.scala
Tools/spell_checker.scala
Tools/task_statistics.scala
--- a/src/Tools/VSCode/src/protocol.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Tools/VSCode/src/protocol.scala Tue Mar 13 19:35:08 2018 +0100
@@ -309,7 +309,7 @@
doc <- JSON.value(params, "textDocument")
uri <- JSON.string(doc, "uri")
version <- JSON.long(doc, "version")
- changes <- JSON.array(params, "contentChanges", unapply_change _)
+ changes <- JSON.list(params, "contentChanges", unapply_change _)
} yield (Url.absolute_file(uri), version, changes)
case _ => None
}
--- a/src/Tools/VSCode/src/server.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Tools/VSCode/src/server.scala Tue Mar 13 19:35:08 2018 +0100
@@ -252,8 +252,8 @@
val try_session =
try {
- if (!Build.build(options = options, build_heap = true, no_build = true,
- system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
+ if (!Build.build(options, build_heap = true, no_build = true,
+ system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
{
val start_msg = "Build started for Isabelle/" + session_name + " ..."
val fail_msg = "Session build failed -- prover process remains inactive!"
@@ -261,7 +261,7 @@
val progress = channel.make_progress(verbose = true)
progress.echo(start_msg); channel.writeln(start_msg)
- if (!Build.build(options = options, progress = progress, build_heap = true,
+ if (!Build.build(options, progress = progress, build_heap = true,
system_mode = system_mode, dirs = session_dirs, sessions = List(session_name)).ok)
{
progress.echo(fail_msg); error(fail_msg)
--- a/src/Tools/jEdit/src/jedit_sessions.scala Mon Mar 12 21:03:57 2018 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Tue Mar 13 19:35:08 2018 +0100
@@ -124,8 +124,8 @@
{
val mode = session_build_mode()
- Build.build(options = session_options(options), progress = progress,
- build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
+ Build.build(session_options(options), progress = progress, build_heap = true,
+ no_build = no_build, system_mode = mode == "" || mode == "system",
dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
sessions = List(PIDE.resources.session_name)).rc
}