tuned signature -- prover-independence is presently theoretical;
authorwenzelm
Tue Aug 02 18:45:34 2016 +0200 (2016-08-02 ago)
changeset 6358468751fe1c036
parent 63583 a39baba12732
child 63585 f4a308fdf664
tuned signature -- prover-independence is presently theoretical;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 18:44:37 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 18:45:34 2016 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4    val keywords: Keyword.Keywords = Keyword.Keywords.empty,
     1.5    val completion: Completion = Completion.empty,
     1.6    val language_context: Completion.Language_Context = Completion.Language_Context.outer,
     1.7 -  val has_tokens: Boolean = true) extends Prover.Syntax
     1.8 +  val has_tokens: Boolean = true)
     1.9  {
    1.10    /** syntax content **/
    1.11  
    1.12 @@ -119,7 +119,7 @@
    1.13  
    1.14    /* merge */
    1.15  
    1.16 -  def ++ (other: Prover.Syntax): Prover.Syntax =
    1.17 +  def ++ (other: Outer_Syntax): Outer_Syntax =
    1.18      if (this eq other) this
    1.19      else {
    1.20        val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
     2.1 --- a/src/Pure/PIDE/command.scala	Tue Aug 02 18:44:37 2016 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 02 18:45:34 2016 +0200
     2.3 @@ -326,7 +326,7 @@
     2.4      }
     2.5      else None
     2.6  
     2.7 -  def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
     2.8 +  def span_files(syntax: Outer_Syntax, span: Command_Span.Span): (List[String], Int) =
     2.9      syntax.load_command(span.name) match {
    2.10        case Some(exts) =>
    2.11          find_file(clean_tokens(span.content)) match {
    2.12 @@ -340,7 +340,7 @@
    2.13  
    2.14    def blobs_info(
    2.15      resources: Resources,
    2.16 -    syntax: Prover.Syntax,
    2.17 +    syntax: Outer_Syntax,
    2.18      get_blob: Document.Node.Name => Option[Document.Blob],
    2.19      can_import: Document.Node.Name => Boolean,
    2.20      node_name: Document.Node.Name,
     3.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 02 18:44:37 2016 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 02 18:45:34 2016 +0200
     3.3 @@ -245,7 +245,7 @@
     3.4    final class Node private(
     3.5      val get_blob: Option[Document.Blob] = None,
     3.6      val header: Node.Header = Node.no_header,
     3.7 -    val syntax: Option[Prover.Syntax] = None,
     3.8 +    val syntax: Option[Outer_Syntax] = None,
     3.9      val text_perspective: Text.Perspective = Text.Perspective.empty,
    3.10      val perspective: Node.Perspective_Command = Node.no_perspective_command,
    3.11      _commands: Node.Commands = Node.Commands.empty)
    3.12 @@ -269,7 +269,7 @@
    3.13      def update_header(new_header: Node.Header): Node =
    3.14        new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
    3.15  
    3.16 -    def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
    3.17 +    def update_syntax(new_syntax: Option[Outer_Syntax]): Node =
    3.18        new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
    3.19  
    3.20      def update_perspective(
     4.1 --- a/src/Pure/PIDE/prover.scala	Tue Aug 02 18:44:37 2016 +0200
     4.2 +++ b/src/Pure/PIDE/prover.scala	Tue Aug 02 18:45:34 2016 +0200
     4.3 @@ -13,19 +13,6 @@
     4.4  
     4.5  object Prover
     4.6  {
     4.7 -  /* syntax */
     4.8 -
     4.9 -  trait Syntax
    4.10 -  {
    4.11 -    def ++ (other: Syntax): Syntax
    4.12 -    def add_keywords(keywords: Thy_Header.Keywords): Syntax
    4.13 -    def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Syntax
    4.14 -    def parse_spans(input: CharSequence): List[Command_Span.Span]
    4.15 -    def load_command(name: String): Option[List[String]]
    4.16 -    def load_commands_in(text: String): Boolean
    4.17 -  }
    4.18 -
    4.19 -
    4.20    /* underlying system process */
    4.21  
    4.22    trait System_Process
     5.1 --- a/src/Pure/PIDE/resources.scala	Tue Aug 02 18:44:37 2016 +0200
     5.2 +++ b/src/Pure/PIDE/resources.scala	Tue Aug 02 18:45:34 2016 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4  class Resources(
     5.5    val loaded_theories: Set[String],
     5.6    val known_theories: Map[String, Document.Node.Name],
     5.7 -  val base_syntax: Prover.Syntax)
     5.8 +  val base_syntax: Outer_Syntax)
     5.9  {
    5.10    /* document node names */
    5.11  
    5.12 @@ -55,7 +55,7 @@
    5.13  
    5.14    /* theory files */
    5.15  
    5.16 -  def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
    5.17 +  def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
    5.18      if (syntax.load_commands_in(text)) {
    5.19        val spans = syntax.parse_spans(text)
    5.20        spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
     6.1 --- a/src/Pure/PIDE/session.scala	Tue Aug 02 18:44:37 2016 +0200
     6.2 +++ b/src/Pure/PIDE/session.scala	Tue Aug 02 18:45:34 2016 +0200
     6.3 @@ -237,7 +237,7 @@
     6.4    private val global_state = Synchronized(Document.State.init)
     6.5    def current_state(): Document.State = global_state.value
     6.6  
     6.7 -  def recent_syntax(name: Document.Node.Name): Prover.Syntax =
     6.8 +  def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     6.9      global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
    6.10      resources.base_syntax
    6.11  
     7.1 --- a/src/Pure/Thy/thy_info.scala	Tue Aug 02 18:44:37 2016 +0200
     7.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Aug 02 18:45:34 2016 +0200
     7.3 @@ -82,7 +82,7 @@
     7.4        header_errors ::: import_errors
     7.5      }
     7.6  
     7.7 -    lazy val syntax: Prover.Syntax =
     7.8 +    lazy val syntax: Outer_Syntax =
     7.9        resources.base_syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    7.10  
    7.11      def loaded_theories: Set[String] =
     8.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 18:44:37 2016 +0200
     8.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 18:45:34 2016 +0200
     8.3 @@ -158,7 +158,7 @@
     8.4  
     8.5    private def reparse_spans(
     8.6      resources: Resources,
     8.7 -    syntax: Prover.Syntax,
     8.8 +    syntax: Outer_Syntax,
     8.9      get_blob: Document.Node.Name => Option[Document.Blob],
    8.10      can_import: Document.Node.Name => Boolean,
    8.11      node_name: Document.Node.Name,
    8.12 @@ -204,7 +204,7 @@
    8.13  
    8.14    private def text_edit(
    8.15      resources: Resources,
    8.16 -    syntax: Prover.Syntax,
    8.17 +    syntax: Outer_Syntax,
    8.18      get_blob: Document.Node.Name => Option[Document.Blob],
    8.19      can_import: Document.Node.Name => Boolean,
    8.20      reparse_limit: Int,