--- 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 */