diff -r bc118a32a870 -r 22f533e6a049 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Pure/PIDE/prover.scala	Thu Apr 03 20:53:35 2014 +0200
@@ -9,6 +9,22 @@
 
 object Prover
 {
+  /* syntax */
+
+  object Syntax
+  {
+    val empty: Syntax = Outer_Syntax.empty
+  }
+
+  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
@@ -56,6 +72,7 @@
   }
 }
 
+
 trait Prover
 {
   /* text and tree data */