# HG changeset patch
# User wenzelm
# Date 1396551215 -7200
# Node ID 22f533e6a049f4f29e78ca15993b3bd6b89b9bf6
# Parent  bc118a32a870c1e011fa1fb8cf3afb4045b25040
more abstract Prover.Syntax, as proposed by Carst Tankink;

diff -r bc118a32a870 -r 22f533e6a049 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Apr 03 20:53:35 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 bc118a32a870 -r 22f533e6a049 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Apr 03 20:53:35 2014 +0200
@@ -317,13 +317,13 @@
   {
     val init: Version = new Version()
 
-    def make(syntax: Outer_Syntax, nodes: Nodes): Version =
+    def make(syntax: 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: Prover.Syntax = Prover.Syntax.empty,
     val nodes: Nodes = Nodes.empty)
   {
     def is_init: Boolean = id == Document_ID.none
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 */
diff -r bc118a32a870 -r 22f533e6a049 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Apr 03 20:53:35 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 loaded_files(syntax: Outer_Syntax, text: String): List[String] =
-  {
-    if (syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
+  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 =
   {
diff -r bc118a32a870 -r 22f533e6a049 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Apr 03 20:53:35 2014 +0200
@@ -222,10 +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
+    if (version.is_init) resources.base_syntax  // FIXME
     else version.syntax
   }
 
diff -r bc118a32a870 -r 22f533e6a049 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Pure/Thy/thy_info.scala	Thu Apr 03 20:53:35 2014 +0200
@@ -31,7 +31,7 @@
     name: Document.Node.Name,
     header: Document.Node.Header)
   {
-    def loaded_files(syntax: Outer_Syntax): List[String] =
+    def loaded_files(syntax: Prover.Syntax): List[String] =
     {
       val string = resources.with_thy_text(name, _.toString)
       resources.loaded_files(syntax, string)
@@ -80,7 +80,7 @@
       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 }
diff -r bc118a32a870 -r 22f533e6a049 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Apr 03 20:53:35 2014 +0200
@@ -153,10 +153,10 @@
   /** header edits: structure and outer syntax **/
 
   private def header_edits(
-    base_syntax: Outer_Syntax,
+    base_syntax: Prover.Syntax,
     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
@@ -245,7 +245,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 +259,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 +291,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 +326,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 +354,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 +398,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 =
diff -r bc118a32a870 -r 22f533e6a049 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Pure/Tools/build.scala	Thu Apr 03 20:53:35 2014 +0200
@@ -441,7 +441,7 @@
 
             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 loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
 
diff -r bc118a32a870 -r 22f533e6a049 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Apr 03 20:17:12 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Apr 03 20:53:35 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)