tuned signature;
authorwenzelm
Tue Aug 07 13:21:29 2012 +0200 (2012-08-07)
changeset 48706e2b512024eab
parent 48705 dd32321d6eef
child 48707 ba531af91148
tuned signature;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/document.scala
src/Pure/System/build.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 12:35:24 2012 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 13:21:29 2012 +0200
     1.3 @@ -34,8 +34,6 @@
     1.4      result.toString
     1.5    }
     1.6  
     1.7 -  type Decl = (String, Option[(String, List[String])])
     1.8 -
     1.9    val empty: Outer_Syntax = new Outer_Syntax()
    1.10    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
    1.11  }
    1.12 @@ -61,10 +59,15 @@
    1.13  
    1.14    def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
    1.15    def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    1.16 -  def + (decl: Outer_Syntax.Decl): Outer_Syntax =
    1.17 -    decl match {
    1.18 -      case ((name, Some((kind, _)))) => this + (name, kind)
    1.19 -      case ((name, None)) => this + name
    1.20 +
    1.21 +  def add_keywords(header: Document.Node_Header): Outer_Syntax =
    1.22 +    header match {
    1.23 +      case Exn.Res(deps) =>
    1.24 +        (this /: deps.keywords) {
    1.25 +          case (syntax, ((name, Some((kind, _))))) => syntax + (name, kind)
    1.26 +          case (syntax, ((name, None))) => syntax + name
    1.27 +        }
    1.28 +      case Exn.Exn(_) => this
    1.29      }
    1.30  
    1.31    def is_command(name: String): Boolean =
     2.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 07 12:35:24 2012 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 07 13:21:29 2012 +0200
     2.3 @@ -41,7 +41,7 @@
     2.4    {
     2.5      sealed case class Deps(
     2.6        imports: List[Name],
     2.7 -      keywords: List[Outer_Syntax.Decl],
     2.8 +      keywords: Thy_Header.Keywords,
     2.9        uses: List[(String, Boolean)])
    2.10  
    2.11      object Name
    2.12 @@ -125,7 +125,7 @@
    2.13      def imports: List[Node.Name] =
    2.14        header match { case Exn.Res(deps) => deps.imports case _ => Nil }
    2.15  
    2.16 -    def keywords: List[Outer_Syntax.Decl] =
    2.17 +    def keywords: Thy_Header.Keywords =
    2.18        header match { case Exn.Res(deps) => deps.keywords case _ => Nil }
    2.19  
    2.20  
     3.1 --- a/src/Pure/System/build.scala	Tue Aug 07 12:35:24 2012 +0200
     3.2 +++ b/src/Pure/System/build.scala	Tue Aug 07 13:21:29 2012 +0200
     3.3 @@ -358,9 +358,7 @@
     3.4                  map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
     3.5  
     3.6            val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
     3.7 -
     3.8 -          val keywords = thy_deps.map({ case (_, Exn.Res(h)) => h.keywords case _ => Nil }).flatten
     3.9 -          val syntax = (parent_syntax /: keywords)(_ + _)
    3.10 +          val syntax = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
    3.11  
    3.12            val all_files =
    3.13              thy_deps.map({ case (n, h) =>
     4.1 --- a/src/Pure/Thy/thy_header.scala	Tue Aug 07 12:35:24 2012 +0200
     4.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Aug 07 13:21:29 2012 +0200
     4.3 @@ -107,12 +107,17 @@
     4.4      try { read(reader).map(Standard_System.decode_permissive_utf8) }
     4.5      finally { reader.close }
     4.6    }
     4.7 +
     4.8 +
     4.9 +  /* keywords */
    4.10 +
    4.11 +  type Keywords = List[(String, Option[(String, List[String])])]
    4.12  }
    4.13  
    4.14  
    4.15  sealed case class Thy_Header(
    4.16    name: String, imports: List[String],
    4.17 -  keywords: List[Outer_Syntax.Decl],
    4.18 +  keywords: Thy_Header.Keywords,
    4.19    uses: List[(String, Boolean)])
    4.20  {
    4.21    def map(f: String => String): Thy_Header =
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 12:35:24 2012 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 13:21:29 2012 +0200
     5.3 @@ -153,7 +153,7 @@
     5.4  
     5.5      val syntax =
     5.6        if (previous.is_init || updated_keywords)
     5.7 -        (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
     5.8 +        (base_syntax /: nodes.entries) { case (syn, (_, node)) => syn.add_keywords(node.header) }
     5.9        else previous.syntax
    5.10  
    5.11      val reparse =