tuned signature -- prover-independence is presently theoretical;

--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 18:44:37 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 18:45:34 2016 +0200
@@ -76,7 +76,7 @@
   val keywords: Keyword.Keywords = Keyword.Keywords.empty,
   val completion: Completion = Completion.empty,
   val language_context: Completion.Language_Context = Completion.Language_Context.outer,
-  val has_tokens: Boolean = true) extends Prover.Syntax
+  val has_tokens: Boolean = true)
 {
   /** syntax content **/
 
@@ -119,7 +119,7 @@
 
   /* merge */
 
-  def ++ (other: Prover.Syntax): Prover.Syntax =
+  def ++ (other: Outer_Syntax): Outer_Syntax =
     if (this eq other) this
     else {
       val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords

--- a/src/Pure/PIDE/command.scala	Tue Aug 02 18:44:37 2016 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 02 18:45:34 2016 +0200
@@ -326,7 +326,7 @@
     }
     else None
 
-  def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
+  def span_files(syntax: Outer_Syntax, span: Command_Span.Span): (List[String], Int) =
     syntax.load_command(span.name) match {
       case Some(exts) =>
         find_file(clean_tokens(span.content)) match {
@@ -340,7 +340,7 @@
 
   def blobs_info(
     resources: Resources,
-    syntax: Prover.Syntax,
+    syntax: Outer_Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,

--- a/src/Pure/PIDE/document.scala	Tue Aug 02 18:44:37 2016 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 02 18:45:34 2016 +0200
@@ -245,7 +245,7 @@
   final class Node private(
     val get_blob: Option[Document.Blob] = None,
     val header: Node.Header = Node.no_header,
-    val syntax: Option[Prover.Syntax] = None,
+    val syntax: Option[Outer_Syntax] = None,
     val text_perspective: Text.Perspective = Text.Perspective.empty,
     val perspective: Node.Perspective_Command = Node.no_perspective_command,
     _commands: Node.Commands = Node.Commands.empty)
@@ -269,7 +269,7 @@
     def update_header(new_header: Node.Header): Node =
       new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
 
-    def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
+    def update_syntax(new_syntax: Option[Outer_Syntax]): Node =
       new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
 
     def update_perspective(

--- a/src/Pure/PIDE/prover.scala	Tue Aug 02 18:44:37 2016 +0200
+++ b/src/Pure/PIDE/prover.scala	Tue Aug 02 18:45:34 2016 +0200
@@ -13,19 +13,6 @@
 
 object Prover
 {
-  /* syntax */
-
-  trait Syntax
-  {
-    def ++ (other: Syntax): Syntax
-    def add_keywords(keywords: Thy_Header.Keywords): Syntax
-    def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Syntax
-    def parse_spans(input: CharSequence): List[Command_Span.Span]
-    def load_command(name: String): Option[List[String]]
-    def load_commands_in(text: String): Boolean
-  }
-
-
   /* underlying system process */
 
   trait System_Process

--- a/src/Pure/PIDE/resources.scala	Tue Aug 02 18:44:37 2016 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Aug 02 18:45:34 2016 +0200
@@ -23,7 +23,7 @@
 class Resources(
   val loaded_theories: Set[String],
   val known_theories: Map[String, Document.Node.Name],
-  val base_syntax: Prover.Syntax)
+  val base_syntax: Outer_Syntax)
 {
   /* document node names */
 
@@ -55,7 +55,7 @@
 
   /* theory files */
 
-  def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
+  def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
     if (syntax.load_commands_in(text)) {
       val spans = syntax.parse_spans(text)
       spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList

--- a/src/Pure/PIDE/session.scala	Tue Aug 02 18:44:37 2016 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Aug 02 18:45:34 2016 +0200
@@ -237,7 +237,7 @@
   private val global_state = Synchronized(Document.State.init)
   def current_state(): Document.State = global_state.value
 
-  def recent_syntax(name: Document.Node.Name): Prover.Syntax =
+  def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
     resources.base_syntax
 

--- a/src/Pure/Thy/thy_info.scala	Tue Aug 02 18:44:37 2016 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Aug 02 18:45:34 2016 +0200
@@ -82,7 +82,7 @@
       header_errors ::: import_errors
     }
 
-    lazy val syntax: Prover.Syntax =
+    lazy val syntax: Outer_Syntax =
       resources.base_syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
     def loaded_theories: Set[String] =

--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 18:44:37 2016 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 18:45:34 2016 +0200
@@ -158,7 +158,7 @@
 
   private def reparse_spans(
     resources: Resources,
-    syntax: Prover.Syntax,
+    syntax: Outer_Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     node_name: Document.Node.Name,
@@ -204,7 +204,7 @@
 
   private def text_edit(
     resources: Resources,
-    syntax: Prover.Syntax,
+    syntax: Outer_Syntax,
     get_blob: Document.Node.Name => Option[Document.Blob],
     can_import: Document.Node.Name => Boolean,
     reparse_limit: Int,