--- 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)
--- 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
--- 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 */
--- 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 =
{
--- 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
}
--- 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 }
--- 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 =
--- 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
--- 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)