--- a/etc/symbols Thu Apr 03 17:26:45 2014 +0100
+++ b/etc/symbols Thu Apr 03 22:04:57 2014 +0200
@@ -154,7 +154,7 @@
\<rat> code: 0x00211a group: letter
\<real> code: 0x00211d group: letter
\<int> code: 0x002124 group: letter
-\<leftarrow> code: 0x002190 group: arrow abbrev: <.
+\<leftarrow> code: 0x002190 group: arrow abbrev: <. abbrev: <-
\<longleftarrow> code: 0x0027f5 group: arrow abbrev: <.
\<rightarrow> code: 0x002192 group: arrow abbrev: .> abbrev: ->
\<longrightarrow> code: 0x0027f6 group: arrow abbrev: .> abbrev: -->
--- a/src/Pure/Isar/outer_syntax.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Thu Apr 03 22:04:57 2014 +0200
@@ -44,7 +44,7 @@
lexicon: Scan.Lexicon = Scan.Lexicon.empty,
val completion: Completion = Completion.empty,
val language_context: Completion.Language_Context = Completion.Language_Context.outer,
- val has_tokens: Boolean = true)
+ val has_tokens: Boolean = true) extends Prover.Syntax
{
override def toString: String =
(for ((name, (kind, files)) <- keywords) yield {
@@ -66,6 +66,9 @@
val load_commands: List[(String, List[String])] =
(for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
+ def load_commands_in(text: String): Boolean =
+ load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+
def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
{
val keywords1 = keywords + (name -> kind)
--- a/src/Pure/PIDE/command.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/PIDE/command.scala Thu Apr 03 22:04:57 2014 +0200
@@ -109,7 +109,18 @@
results: Results = Results.empty,
markups: Markups = Markups.empty)
{
- lazy val protocol_status: Protocol.Status = Protocol.Status.make(status.iterator)
+ lazy val protocol_status: Protocol.Status =
+ {
+ val warnings =
+ if (results.iterator.exists(p => Protocol.is_warning(p._2)))
+ List(Markup(Markup.WARNING, Nil))
+ else Nil
+ val errors =
+ if (results.iterator.exists(p => Protocol.is_error(p._2)))
+ List(Markup(Markup.ERROR, Nil))
+ else Nil
+ Protocol.Status.make((warnings ::: errors ::: status).iterator)
+ }
def markup(index: Markup_Index): Markup_Tree = markups(index)
@@ -126,7 +137,7 @@
private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
{
val markups1 =
- if (status || Protocol.status_elements(m.info.name))
+ if (status || Protocol.liberal_status_elements(m.info.name))
markups.add(Markup_Index(true, file_name), m)
else markups
copy(markups = markups1.add(Markup_Index(false, file_name), m))
--- a/src/Pure/PIDE/document.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/PIDE/document.scala Thu Apr 03 22:04:57 2014 +0200
@@ -317,17 +317,15 @@
{
val init: Version = new Version()
- def make(syntax: Outer_Syntax, nodes: Nodes): Version =
+ def make(syntax: Option[Prover.Syntax], nodes: Nodes): Version =
new Version(Document_ID.make(), syntax, nodes)
}
final class Version private(
val id: Document_ID.Version = Document_ID.none,
- val syntax: Outer_Syntax = Outer_Syntax.empty,
+ val syntax: Option[Prover.Syntax] = None,
val nodes: Nodes = Nodes.empty)
{
- def is_init: Boolean = id == Document_ID.none
-
override def toString: String = "Version(" + id + ")"
}
--- a/src/Pure/PIDE/protocol.ML Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/PIDE/protocol.ML Thu Apr 03 22:04:57 2014 +0200
@@ -8,11 +8,11 @@
struct
val _ =
- Isabelle_Process.protocol_command "Isabelle_Process.echo"
+ Isabelle_Process.protocol_command "Prover.echo"
(fn args => List.app writeln args);
val _ =
- Isabelle_Process.protocol_command "Isabelle_Process.options"
+ Isabelle_Process.protocol_command "Prover.options"
(fn [options_yxml] =>
let val options = Options.decode (YXML.parse_body options_yxml) in
Options.set_default options;
--- a/src/Pure/PIDE/protocol.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala Thu Apr 03 22:04:57 2014 +0200
@@ -47,6 +47,7 @@
{
var touched = false
var accepted = false
+ var warned = false
var failed = false
var forks = 0
var runs = 0
@@ -57,11 +58,12 @@
case Markup.JOINED => forks -= 1
case Markup.RUNNING => touched = true; runs += 1
case Markup.FINISHED => runs -= 1
- case Markup.FAILED => failed = true
+ case Markup.WARNING => warned = true
+ case Markup.FAILED | Markup.ERROR => failed = true
case _ =>
}
}
- Status(touched, accepted, failed, forks, runs)
+ Status(touched, accepted, warned, failed, forks, runs)
}
val empty = make(Iterator.empty)
@@ -77,26 +79,33 @@
sealed case class Status(
private val touched: Boolean,
private val accepted: Boolean,
+ private val warned: Boolean,
private val failed: Boolean,
forks: Int,
runs: Int)
{
def + (that: Status): Status =
- Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
- forks + that.forks, runs + that.runs)
+ Status(
+ touched || that.touched,
+ accepted || that.accepted,
+ warned || that.warned,
+ failed || that.failed,
+ forks + that.forks,
+ runs + that.runs)
def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
def is_running: Boolean = runs != 0
def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
+ def is_warned: Boolean = is_finished && warned
def is_failed: Boolean = failed
}
- val command_status_elements =
+ val proper_status_elements =
Document.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
Markup.FINISHED, Markup.FAILED)
- val status_elements =
- command_status_elements + Markup.WARNING + Markup.ERROR
+ val liberal_status_elements =
+ proper_status_elements + Markup.WARNING + Markup.ERROR
/* command timing */
@@ -136,10 +145,8 @@
val status = Status.merge(states.iterator.map(_.protocol_status))
if (status.is_running) running += 1
- else if (status.is_finished) {
- val warning = states.exists(st => st.results.iterator.exists(p => is_warning(p._2)))
- if (warning) warned += 1 else finished += 1
- }
+ else if (status.is_warned) warned += 1
+ else if (status.is_finished) finished += 1
else if (status.is_failed) failed += 1
else unprocessed += 1
}
@@ -325,15 +332,18 @@
}
-trait Protocol extends Isabelle_Process
+trait Protocol extends Prover
{
- /* inlined files */
+ /* options */
+
+ def options(opts: Options): Unit =
+ protocol_command("Prover.options", YXML.string_of_body(opts.encode))
+
+
+ /* interned items */
def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
- protocol_command_raw("Document.define_blob", Bytes(digest.toString), bytes)
-
-
- /* commands */
+ protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
def define_command(command: Command): Unit =
{
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/prover.scala Thu Apr 03 22:04:57 2014 +0200
@@ -0,0 +1,111 @@
+/* Title: Pure/PIDE/prover.scala
+ Author: Makarius
+
+General prover operations.
+*/
+
+package isabelle
+
+
+object Prover
+{
+ /* syntax */
+
+ trait Syntax
+ {
+ def add_keywords(keywords: Thy_Header.Keywords): Syntax
+ def scan(input: CharSequence): List[Token]
+ def load(span: List[Token]): Option[List[String]]
+ def load_commands_in(text: String): Boolean
+ }
+
+
+ /* messages */
+
+ sealed abstract class Message
+
+ class Input(val name: String, val args: List[String]) extends Message
+ {
+ override def toString: String =
+ XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
+ args.map(s =>
+ List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
+ }
+
+ class Output(val message: XML.Elem) extends Message
+ {
+ def kind: String = message.markup.name
+ def properties: Properties.T = message.markup.properties
+ def body: XML.Body = message.body
+
+ def is_init = kind == Markup.INIT
+ def is_exit = kind == Markup.EXIT
+ def is_stdout = kind == Markup.STDOUT
+ def is_stderr = kind == Markup.STDERR
+ def is_system = kind == Markup.SYSTEM
+ def is_status = kind == Markup.STATUS
+ def is_report = kind == Markup.REPORT
+ def is_syslog = is_init || is_exit || is_system || is_stderr
+
+ override def toString: String =
+ {
+ val res =
+ if (is_status || is_report) message.body.map(_.toString).mkString
+ else Pretty.string_of(message.body)
+ if (properties.isEmpty)
+ kind.toString + " [[" + res + "]]"
+ else
+ kind.toString + " " +
+ (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
+ }
+ }
+
+ class Protocol_Output(props: Properties.T, val bytes: Bytes)
+ extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
+ {
+ lazy val text: String = bytes.toString
+ }
+}
+
+
+trait Prover
+{
+ /* text and tree data */
+
+ def encode(s: String): String
+ def decode(s: String): String
+
+ object Encode
+ {
+ val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
+ }
+
+ def xml_cache: XML.Cache
+
+
+ /* process management */
+
+ def join(): Unit
+ def terminate(): Unit
+
+ def protocol_command_bytes(name: String, args: Bytes*): Unit
+ def protocol_command(name: String, args: String*): Unit
+
+
+ /* PIDE protocol commands */
+
+ def options(opts: Options): Unit
+
+ def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit
+ def define_command(command: Command): Unit
+
+ def discontinue_execution(): Unit
+ def cancel_exec(id: Document_ID.Exec): Unit
+
+ def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
+ edits: List[Document.Edit_Command]): Unit
+ def remove_versions(versions: List[Document.Version]): Unit
+
+ def dialog_result(serial: Long, result: String): Unit
+}
+
--- a/src/Pure/PIDE/resources.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/PIDE/resources.scala Thu Apr 03 22:04:57 2014 +0200
@@ -18,7 +18,7 @@
}
-class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
+class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Prover.Syntax)
{
/* document node names */
@@ -50,14 +50,12 @@
/* theory files */
- def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
- syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
-
- def body_files(syntax: Outer_Syntax, text: String): List[String] =
- {
- val spans = Thy_Syntax.parse_spans(syntax.scan(text))
- spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
- }
+ def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
+ if (syntax.load_commands_in(text)) {
+ val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+ spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
+ }
+ else Nil
def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
{
@@ -101,5 +99,11 @@
Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
def commit(change: Session.Change) { }
+
+
+ /* prover process */
+
+ def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
+ new Isabelle_Process(receiver, args) with Protocol
}
--- a/src/Pure/PIDE/session.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/PIDE/session.scala Thu Apr 03 22:04:57 2014 +0200
@@ -51,17 +51,15 @@
/* protocol handlers */
- type Prover = Isabelle_Process with Protocol
-
abstract class Protocol_Handler
{
def stop(prover: Prover): Unit = {}
- val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean]
+ val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
}
class Protocol_Handlers(
handlers: Map[String, Session.Protocol_Handler] = Map.empty,
- functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty)
+ functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
{
def get(name: String): Option[Protocol_Handler] = handlers.get(name)
@@ -81,7 +79,7 @@
val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
val new_functions =
for ((a, f) <- new_handler.functions.toList) yield
- (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg))
+ (a, (msg: Prover.Protocol_Output) => f(prover, msg))
val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
@@ -98,7 +96,7 @@
new Protocol_Handlers(handlers2, functions2)
}
- def invoke(msg: Isabelle_Process.Protocol_Output): Boolean =
+ def invoke(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
case Markup.Function(a) if functions.isDefinedAt(a) =>
try { functions(a)(msg) }
@@ -146,9 +144,9 @@
val raw_edits = new Event_Bus[Session.Raw_Edits]
val commands_changed = new Event_Bus[Session.Commands_Changed]
val phase_changed = new Event_Bus[Session.Phase]
- val syslog_messages = new Event_Bus[Isabelle_Process.Output]
- val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
- val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
+ val syslog_messages = new Event_Bus[Prover.Output]
+ val raw_output_messages = new Event_Bus[Prover.Output]
+ val all_messages = new Event_Bus[Prover.Message] // potential bottle-neck
val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
@@ -224,11 +222,10 @@
private val global_state = Volatile(Document.State.init)
def current_state(): Document.State = global_state()
- def recent_syntax(): Outer_Syntax =
+ def recent_syntax(): Prover.Syntax =
{
val version = current_state().recent_finished.version.get_finished
- if (version.is_init) resources.base_syntax
- else version.syntax
+ version.syntax getOrElse resources.base_syntax
}
def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
@@ -258,10 +255,10 @@
/* actor messages */
- private case class Start(args: List[String])
+ private case class Start(name: String, args: List[String])
private case class Cancel_Exec(exec_id: Document_ID.Exec)
private case class Protocol_Command(name: String, args: List[String])
- private case class Messages(msgs: List[Isabelle_Process.Message])
+ private case class Messages(msgs: List[Prover.Message])
private case class Update_Options(options: Options)
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
@@ -275,22 +272,22 @@
object receiver
{
- private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+ private var buffer = new mutable.ListBuffer[Prover.Message]
private def flush(): Unit = synchronized {
if (!buffer.isEmpty) {
val msgs = buffer.toList
this_actor ! Messages(msgs)
- buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+ buffer = new mutable.ListBuffer[Prover.Message]
}
}
- def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
+ def invoke(msg: Prover.Message): Unit = synchronized {
msg match {
- case _: Isabelle_Process.Input =>
+ case _: Prover.Input =>
buffer += msg
- case output: Isabelle_Process.Protocol_Output if output.properties == Markup.Flush =>
+ case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
flush()
- case output: Isabelle_Process.Output =>
+ case output: Prover.Output =>
buffer += msg
if (output.is_syslog)
syslog >> (queue =>
@@ -307,7 +304,7 @@
def cancel() { timer.cancel() }
}
- var prover: Option[Session.Prover] = None
+ var prover: Option[Prover] = None
/* delayed command changes */
@@ -410,7 +407,7 @@
/* prover output */
- def handle_output(output: Isabelle_Process.Output)
+ def handle_output(output: Prover.Output)
//{{{
{
def bad_output()
@@ -431,7 +428,7 @@
}
output match {
- case msg: Isabelle_Process.Protocol_Output =>
+ case msg: Prover.Protocol_Output =>
val handled = _protocol_handlers.invoke(msg)
if (!handled) {
msg.properties match {
@@ -505,10 +502,10 @@
receiveWithin(delay_commands_changed.flush_timeout) {
case TIMEOUT => delay_commands_changed.flush()
- case Start(args) if prover.isEmpty =>
+ case Start(name, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
- prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
+ prover = Some(resources.start_prover(receiver.invoke _, name, args))
}
case Stop =>
@@ -541,17 +538,17 @@
case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
prover.get.dialog_result(serial, result)
- handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(id, serial, result)))
+ handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
case Protocol_Command(name, args) if prover.isDefined =>
prover.get.protocol_command(name, args:_*)
case Messages(msgs) =>
msgs foreach {
- case input: Isabelle_Process.Input =>
+ case input: Prover.Input =>
all_messages.event(input)
- case output: Isabelle_Process.Output =>
+ case output: Prover.Output =>
if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
else handle_output(output)
if (output.is_syslog) syslog_messages.event(output)
@@ -572,9 +569,9 @@
/* actions */
- def start(args: List[String])
+ def start(name: String, args: List[String])
{
- session_actor ! Start(args)
+ session_actor ! Start(name, args)
}
def stop()
--- a/src/Pure/System/invoke_scala.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/System/invoke_scala.scala Thu Apr 03 22:04:57 2014 +0200
@@ -72,24 +72,22 @@
{
private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
- private def fulfill(prover: Session.Prover,
- id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = synchronized
- {
- if (futures.isDefinedAt(id)) {
- prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
- futures -= id
+ private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
+ synchronized
+ {
+ if (futures.isDefinedAt(id)) {
+ prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
+ futures -= id
+ }
}
- }
- private def cancel(prover: Session.Prover,
- id: String, future: java.util.concurrent.Future[Unit])
+ private def cancel(prover: Prover, id: String, future: java.util.concurrent.Future[Unit])
{
future.cancel(true)
fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
}
- private def invoke_scala(
- prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized
+ private def invoke_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
{
msg.properties match {
case Markup.Invoke_Scala(name, id) =>
@@ -104,8 +102,7 @@
}
}
- private def cancel_scala(
- prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized
+ private def cancel_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
{
msg.properties match {
case Markup.Cancel_Scala(id) =>
@@ -118,7 +115,7 @@
}
}
- override def stop(prover: Session.Prover): Unit = synchronized
+ override def stop(prover: Prover): Unit = synchronized
{
for ((id, future) <- futures) cancel(prover, id, future)
futures = Map.empty
--- a/src/Pure/System/isabelle_process.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/System/isabelle_process.scala Thu Apr 03 22:04:57 2014 +0200
@@ -16,86 +16,28 @@
import Actor._
-object Isabelle_Process
+class Isabelle_Process(
+ receiver: Prover.Message => Unit = Console.println(_),
+ prover_args: List[String] = Nil)
{
- /* messages */
-
- sealed abstract class Message
-
- class Input(name: String, args: List[String]) extends Message
- {
- override def toString: String =
- XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
- args.map(s =>
- List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
- }
-
- class Output(val message: XML.Elem) extends Message
- {
- def kind: String = message.markup.name
- def properties: Properties.T = message.markup.properties
- def body: XML.Body = message.body
-
- def is_init = kind == Markup.INIT
- def is_exit = kind == Markup.EXIT
- def is_stdout = kind == Markup.STDOUT
- def is_stderr = kind == Markup.STDERR
- def is_system = kind == Markup.SYSTEM
- def is_status = kind == Markup.STATUS
- def is_report = kind == Markup.REPORT
- def is_syslog = is_init || is_exit || is_system || is_stderr
-
- override def toString: String =
- {
- val res =
- if (is_status || is_report) message.body.map(_.toString).mkString
- else Pretty.string_of(message.body)
- if (properties.isEmpty)
- kind.toString + " [[" + res + "]]"
- else
- kind.toString + " " +
- (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
- }
- }
-
- class Protocol_Output(props: Properties.T, val bytes: Bytes)
- extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil))
- {
- lazy val text: String = bytes.toString
- }
-}
-
-
-class Isabelle_Process(
- receiver: Isabelle_Process.Message => Unit = Console.println(_),
- arguments: List[String] = Nil)
-{
- import Isabelle_Process._
-
-
- /* text representation */
+ /* text and tree data */
def encode(s: String): String = Symbol.encode(s)
def decode(s: String): String = Symbol.decode(s)
- object Encode
- {
- val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
- }
+ val xml_cache = new XML.Cache()
/* output */
- val xml_cache = new XML.Cache()
-
private def system_output(text: String)
{
- receiver(new Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
+ receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
}
private def protocol_output(props: Properties.T, bytes: Bytes)
{
- receiver(new Protocol_Output(props, bytes))
+ receiver(new Prover.Protocol_Output(props, bytes))
}
private def output(kind: String, props: Properties.T, body: XML.Body)
@@ -104,7 +46,7 @@
val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
val reports = Protocol.message_reports(props, body)
- for (msg <- main :: reports) receiver(new Output(xml_cache.elem(msg)))
+ for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg)))
}
private def exit_message(rc: Int)
@@ -129,6 +71,7 @@
@volatile private var command_input: (Thread, Actor) = null
+
/** process manager **/
def command_line(channel: System_Channel, args: List[String]): List[String] =
@@ -138,12 +81,12 @@
private val process =
try {
- val cmdline = command_line(system_channel, arguments)
+ val cmdline = command_line(system_channel, prover_args)
new Isabelle_System.Managed_Process(null, null, false, cmdline: _*)
}
catch { case e: IOException => system_channel.accepted(); throw(e) }
- val (_, process_result) =
+ private val (_, process_result) =
Simple_Thread.future("process_result") { process.join }
private def terminate_process()
@@ -375,17 +318,15 @@
}
- /** main methods **/
- def protocol_command_raw(name: String, args: Bytes*): Unit =
+ /** protocol commands **/
+
+ def protocol_command_bytes(name: String, args: Bytes*): Unit =
command_input._2 ! Input_Chunks(Bytes(name) :: args.toList)
def protocol_command(name: String, args: String*)
{
- receiver(new Input(name, args.toList))
- protocol_command_raw(name, args.map(Bytes(_)): _*)
+ receiver(new Prover.Input(name, args.toList))
+ protocol_command_bytes(name, args.map(Bytes(_)): _*)
}
-
- def options(opts: Options): Unit =
- protocol_command("Isabelle_Process.options", YXML.string_of_body(opts.encode))
}
--- a/src/Pure/Thy/thy_info.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/Thy/thy_info.scala Thu Apr 03 22:04:57 2014 +0200
@@ -31,12 +31,10 @@
name: Document.Node.Name,
header: Document.Node.Header)
{
- def load_files(syntax: Outer_Syntax): List[String] =
+ def loaded_files(syntax: Prover.Syntax): List[String] =
{
val string = resources.with_thy_text(name, _.toString)
- if (resources.body_files_test(syntax, string))
- resources.body_files(syntax, string)
- else Nil
+ resources.loaded_files(syntax, string)
}
}
@@ -82,17 +80,17 @@
header_errors ::: import_errors
}
- lazy val syntax: Outer_Syntax = resources.base_syntax.add_keywords(keywords)
+ lazy val syntax: Prover.Syntax = resources.base_syntax.add_keywords(keywords)
def loaded_theories: Set[String] =
(resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
- def load_files: List[Path] =
+ def loaded_files: List[Path] =
{
val dep_files =
rev_deps.par.map(dep =>
Exn.capture {
- dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
+ dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
}).toList
((Nil: List[Path]) /: dep_files) {
case (acc_files, files) => Exn.release(files) ::: acc_files
--- a/src/Pure/Thy/thy_syntax.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Thu Apr 03 22:04:57 2014 +0200
@@ -153,10 +153,10 @@
/** header edits: structure and outer syntax **/
private def header_edits(
- base_syntax: Outer_Syntax,
+ resources: Resources,
previous: Document.Version,
edits: List[Document.Edit_Text]):
- (Outer_Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
+ (Prover.Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes,
List[Document.Edit_Command]) =
{
var updated_imports = false
@@ -180,14 +180,16 @@
}
val (syntax, syntax_changed) =
- if (previous.is_init || updated_keywords) {
- val syntax =
- (base_syntax /: nodes.iterator) {
- case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
- }
- (syntax, true)
+ previous.syntax match {
+ case Some(syntax) if !updated_keywords =>
+ (syntax, false)
+ case _ =>
+ val syntax =
+ (resources.base_syntax /: nodes.iterator) {
+ case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
+ }
+ (syntax, true)
}
- else (previous.syntax, false)
val reparse =
if (updated_imports || updated_keywords)
@@ -245,7 +247,7 @@
}
}
- def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
+ def span_files(syntax: Prover.Syntax, span: List[Token]): List[String] =
syntax.load(span) match {
case Some(exts) =>
find_file(span) match {
@@ -259,7 +261,7 @@
def resolve_files(
resources: Resources,
- syntax: Outer_Syntax,
+ syntax: Prover.Syntax,
node_name: Document.Node.Name,
span: List[Token],
get_blob: Document.Node.Name => Option[Document.Blob])
@@ -291,7 +293,7 @@
private def reparse_spans(
resources: Resources,
- syntax: Outer_Syntax,
+ syntax: Prover.Syntax,
get_blob: Document.Node.Name => Option[Document.Blob],
name: Document.Node.Name,
commands: Linear_Set[Command],
@@ -326,7 +328,7 @@
// FIXME somewhat slow
private def recover_spans(
resources: Resources,
- syntax: Outer_Syntax,
+ syntax: Prover.Syntax,
get_blob: Document.Node.Name => Option[Document.Blob],
name: Document.Node.Name,
perspective: Command.Perspective,
@@ -354,7 +356,7 @@
private def consolidate_spans(
resources: Resources,
- syntax: Outer_Syntax,
+ syntax: Prover.Syntax,
get_blob: Document.Node.Name => Option[Document.Blob],
reparse_limit: Int,
name: Document.Node.Name,
@@ -398,7 +400,7 @@
private def text_edit(
resources: Resources,
- syntax: Outer_Syntax,
+ syntax: Prover.Syntax,
get_blob: Document.Node.Name => Option[Document.Blob],
reparse_limit: Int,
node: Document.Node, edit: Document.Edit_Text): Document.Node =
@@ -443,10 +445,10 @@
doc_blobs.get(name) orElse previous.nodes(name).get_blob
val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) =
- header_edits(resources.base_syntax, previous, edits)
+ header_edits(resources, previous, edits)
val (doc_edits, version) =
- if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes))
+ if (edits.isEmpty) (Nil, Document.Version.make(Some(syntax), previous.nodes))
else {
val reparse =
(reparse0 /: nodes0.iterator)({
@@ -485,7 +487,7 @@
nodes += (name -> node2)
}
- (doc_edits.toList, Document.Version.make(syntax, nodes))
+ (doc_edits.toList, Document.Version.make(Some(syntax), nodes))
}
Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version)
--- a/src/Pure/Tools/build.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/Tools/build.scala Thu Apr 03 22:04:57 2014 +0200
@@ -441,12 +441,12 @@
val loaded_theories = thy_deps.loaded_theories
val keywords = thy_deps.keywords
- val syntax = thy_deps.syntax
+ val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
- val body_files = if (inlined_files) thy_deps.load_files else Nil
+ val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
val all_files =
- (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
+ (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
info.files.map(file => info.dir + file)).map(_.expand)
if (list_files) {
--- a/src/Pure/Tools/simplifier_trace.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala Thu Apr 03 22:04:57 2014 +0200
@@ -300,7 +300,7 @@
class Handler extends Session.Protocol_Handler
{
- private def cancel(prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
+ private def cancel(prover: Prover, msg: Prover.Protocol_Output): Boolean =
msg.properties match {
case Markup.Simp_Trace_Cancel(serial) =>
manager ! Cancel(serial)
@@ -309,7 +309,7 @@
false
}
- override def stop(prover: Session.Prover) =
+ override def stop(prover: Prover) =
{
manager ! Clear_Memory
manager ! Stop
--- a/src/Pure/Tools/sledgehammer_params.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/Tools/sledgehammer_params.scala Thu Apr 03 22:04:57 2014 +0200
@@ -36,8 +36,7 @@
}
def get_provers: String = synchronized { _provers }
- private def sledgehammer_provers(
- prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
+ private def sledgehammer_provers(prover: Prover, msg: Prover.Protocol_Output): Boolean =
{
update_provers(msg.text)
true
--- a/src/Pure/build-jars Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Pure/build-jars Thu Apr 03 22:04:57 2014 +0200
@@ -52,6 +52,7 @@
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
+ PIDE/prover.scala
PIDE/query_operation.scala
PIDE/resources.scala
PIDE/session.scala
--- a/src/Tools/jEdit/src/isabelle.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Thu Apr 03 22:04:57 2014 +0200
@@ -46,8 +46,10 @@
def mode_syntax(name: String): Option[Outer_Syntax] =
name match {
case "isabelle" | "isabelle-markup" =>
- val syntax = PIDE.session.recent_syntax
- if (syntax == Outer_Syntax.empty) None else Some(syntax)
+ PIDE.session.recent_syntax match {
+ case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
+ case _ => None
+ }
case "isabelle-options" => Some(Options.options_syntax)
case "isabelle-root" => Some(Build.root_syntax)
case "isabelle-ml" => Some(ml_syntax)
--- a/src/Tools/jEdit/src/plugin.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Apr 03 22:04:57 2014 +0200
@@ -293,7 +293,7 @@
if (PIDE.startup_failure.isEmpty) {
message match {
case msg: EditorStarted =>
- PIDE.session.start(Isabelle_Logic.session_args())
+ PIDE.session.start("Isabelle", Isabelle_Logic.session_args())
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
--- a/src/Tools/jEdit/src/protocol_dockable.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Thu Apr 03 22:04:57 2014 +0200
@@ -26,11 +26,11 @@
private val main_actor = actor {
loop {
react {
- case input: Isabelle_Process.Input =>
- Swing_Thread.later { text_area.append(input.toString + "\n") }
+ case input: Prover.Input =>
+ Swing_Thread.later { text_area.append(input.toString + "\n\n") }
- case output: Isabelle_Process.Output =>
- Swing_Thread.later { text_area.append(output.message.toString + "\n") }
+ case output: Prover.Output =>
+ Swing_Thread.later { text_area.append(output.message.toString + "\n\n") }
case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Thu Apr 03 22:04:57 2014 +0200
@@ -26,7 +26,7 @@
private val main_actor = actor {
loop {
react {
- case output: Isabelle_Process.Output =>
+ case output: Prover.Output =>
Swing_Thread.later {
text_area.append(XML.content(output.message))
if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
--- a/src/Tools/jEdit/src/rendering.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Thu Apr 03 22:04:57 2014 +0200
@@ -182,7 +182,7 @@
Document.Elements(Markup.SEPARATOR)
private val background_elements =
- Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
+ Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
active_elements
@@ -292,26 +292,18 @@
if (snapshot.is_outdated) None
else {
val results =
- snapshot.cumulate[(List[Markup], Int)](
- range, (Nil, 0), Protocol.status_elements, _ =>
+ snapshot.cumulate[List[Markup]](range, Nil, Protocol.liberal_status_elements, _ =>
{
- case ((status, pri), Text.Info(_, elem)) =>
- if (Protocol.command_status_elements(elem.name))
- Some((elem.markup :: status), pri)
- else
- Some((status, pri max Rendering.message_pri(elem.name)))
+ case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
}, status = true)
if (results.isEmpty) None
else {
- val status =
- Protocol.Status.make(results.iterator.flatMap(info => info.info._1.iterator))
- val pri = (0 /: results.iterator.map(info => info.info._2))(_ max _)
+ val status = Protocol.Status.make(results.iterator.flatMap(_.info))
if (status.is_running) Some(running_color)
- else if (pri == Rendering.warning_pri) Some(warning_color)
- else if (pri == Rendering.error_pri) Some(error_color)
+ else if (status.is_warned) Some(warning_color)
+ else if (status.is_failed) Some(error_color)
else if (status.is_unprocessed) Some(unprocessed_color)
- else if (status.is_failed) Some(error_color)
else None
}
}
@@ -606,7 +598,7 @@
command_states =>
{
case (((status, color), Text.Info(_, XML.Elem(markup, _))))
- if !status.isEmpty && Protocol.command_status_elements(markup.name) =>
+ if !status.isEmpty && Protocol.proper_status_elements(markup.name) =>
Some((markup :: status, color))
case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
Some((Nil, Some(bad_color)))
--- a/src/Tools/jEdit/src/syslog_dockable.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Thu Apr 03 22:04:57 2014 +0200
@@ -37,7 +37,7 @@
private val main_actor = actor {
loop {
react {
- case output: Isabelle_Process.Output =>
+ case output: Prover.Output =>
if (output.is_syslog) Swing_Thread.later { update_syslog() }
case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
--- a/src/Tools/jEdit/src/theories_dockable.scala Thu Apr 03 17:26:45 2014 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Apr 03 22:04:57 2014 +0200
@@ -15,8 +15,8 @@
import scala.swing.event.{MouseClicked, MouseMoved}
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
-import javax.swing.{JList, BorderFactory}
-import javax.swing.border.{BevelBorder, SoftBevelBorder, EtchedBorder}
+import javax.swing.{JList, BorderFactory, UIManager}
+import javax.swing.border.{BevelBorder, SoftBevelBorder}
import org.gjt.sp.jedit.{View, jEdit}
@@ -26,6 +26,12 @@
/* status */
private val status = new ListView(Nil: List[Document.Node.Name]) {
+ background =
+ {
+ // enforce default value
+ val c = UIManager.getDefaults.getColor("Panel.background")
+ new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
+ }
listenTo(mouse.clicks)
listenTo(mouse.moves)
reactions += {
@@ -109,7 +115,7 @@
private object Node_Renderer_Component extends BorderPanel
{
- opaque = false
+ opaque = true
border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
var node_name = Document.Node.Name.empty
@@ -126,8 +132,13 @@
}
val label = new Label {
+ background = view.getTextArea.getPainter.getBackground
+ foreground = view.getTextArea.getPainter.getForeground
+ border =
+ BorderFactory.createCompoundBorder(
+ BorderFactory.createLineBorder(foreground, 1),
+ BorderFactory.createEmptyBorder(1, 1, 1, 1))
opaque = false
- border = new EtchedBorder(EtchedBorder.RAISED)
xAlignment = Alignment.Leading
override def paintComponent(gfx: Graphics2D)
@@ -138,6 +149,7 @@
gfx.fillRect(x, 0, w, size.height)
}
+ paint_segment(0, size.width, background)
nodes_status.get(node_name) match {
case Some(st) if st.total > 0 =>
val segments =