# HG changeset patch
# User wenzelm
# Date 1396555497 -7200
# Node ID 91a8561a8e358a81ff19a067b0470e9efad3ec5f
# Parent  5fdcfffcc72e5901bc9ca3c86b4c2002d8b58b7b# Parent  0546e036d1c084d569e614a82b9ad7e5e88afc05
merged

diff -r 5fdcfffcc72e -r 91a8561a8e35 etc/symbols
--- 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: -->
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/Isar/outer_syntax.scala
--- 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)
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/PIDE/command.scala
--- 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))
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/PIDE/document.scala
--- 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 + ")"
   }
 
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/PIDE/protocol.ML
--- 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;
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/PIDE/protocol.scala
--- 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 =
   {
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/PIDE/prover.scala
--- /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
+}
+
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/PIDE/resources.scala
--- 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
 }
 
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/PIDE/session.scala
--- 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()
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/System/invoke_scala.scala
--- 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
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/System/isabelle_process.scala
--- 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))
 }
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/Thy/thy_info.scala
--- 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
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/Thy/thy_syntax.scala
--- 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)
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/Tools/build.scala
--- 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) {
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/Tools/simplifier_trace.scala
--- 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
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/Tools/sledgehammer_params.scala
--- 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
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Pure/build-jars
--- 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
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Tools/jEdit/src/isabelle.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)
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Tools/jEdit/src/plugin.scala
--- 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 =>
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Tools/jEdit/src/protocol_dockable.scala
--- 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)
       }
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Tools/jEdit/src/raw_output_dockable.scala
--- 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")
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Tools/jEdit/src/rendering.scala
--- 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)))
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Tools/jEdit/src/syslog_dockable.scala
--- 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)
diff -r 5fdcfffcc72e -r 91a8561a8e35 src/Tools/jEdit/src/theories_dockable.scala
--- 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 =