more direct cumulation of (sparse) keywords;
authorwenzelm
Tue Aug 21 16:56:18 2012 +0200 (2012-08-21)
changeset 4887318b17f15bc62
parent 48872 6124e0d1120a
child 48874 ff9cd47be39b
more direct cumulation of (sparse) keywords;
discontinued slightly odd patching of Pure keywords;
tuned signature;
src/Pure/Isar/outer_syntax.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 21 14:54:29 2012 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 21 16:56:18 2012 +0200
     1.3 @@ -71,8 +71,8 @@
     1.4    def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), name)
     1.5    def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
     1.6  
     1.7 -  def add_keywords(header: Document.Node.Header): Outer_Syntax =
     1.8 -    (this /: header.keywords) {
     1.9 +  def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.10 +    (this /: keywords) {
    1.11        case (syntax, ((name, Some((kind, _))))) =>
    1.12          syntax + (Symbol.decode(name), kind) + (Symbol.encode(name), kind)
    1.13        case (syntax, ((name, None))) =>
     2.1 --- a/src/Pure/Thy/thy_info.scala	Tue Aug 21 14:54:29 2012 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Aug 21 16:56:18 2012 +0200
     2.3 @@ -28,36 +28,30 @@
     2.4  
     2.5    object Dependencies
     2.6    {
     2.7 -    val empty = new Dependencies(Nil, Set.empty)
     2.8 +    val empty = new Dependencies(Nil, Nil, Set.empty)
     2.9    }
    2.10  
    2.11    final class Dependencies private(
    2.12      rev_deps: List[Dep],
    2.13 +    val keywords: Thy_Header.Keywords,
    2.14      val seen: Set[Document.Node.Name])
    2.15    {
    2.16 -    def :: (dep: Dep): Dependencies = new Dependencies(dep :: rev_deps, seen)
    2.17 -    def + (name: Document.Node.Name): Dependencies = new Dependencies(rev_deps, seen = seen + name)
    2.18 +    def :: (dep: Dep): Dependencies =
    2.19 +      new Dependencies(dep :: rev_deps, dep._2.keywords ::: keywords, seen)
    2.20 +
    2.21 +    def + (name: Document.Node.Name): Dependencies =
    2.22 +      new Dependencies(rev_deps, keywords, seen = seen + name)
    2.23  
    2.24      def deps: List[Dep] = rev_deps.reverse
    2.25  
    2.26      def thy_load_commands: List[String] =
    2.27 -      (for ((_, h) <- rev_deps; (cmd, Some(((Keyword.THY_LOAD, _), _))) <- h.keywords) yield cmd) :::
    2.28 +      (for ((cmd, Some(((Keyword.THY_LOAD, _), _))) <- keywords) yield cmd) :::
    2.29          thy_load.base_syntax.thy_load_commands
    2.30  
    2.31      def loaded_theories: Set[String] =
    2.32        (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory }
    2.33  
    2.34 -    def syntax: Outer_Syntax =
    2.35 -      (thy_load.base_syntax /: rev_deps) { case (syn, (name, h)) =>
    2.36 -        val syn1 = syn.add_keywords(h)
    2.37 -        // FIXME avoid hardwired stuff!?
    2.38 -        // FIXME broken?!
    2.39 -        if (name.theory == "Pure")
    2.40 -          syn1 +
    2.41 -            ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
    2.42 -            ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
    2.43 -        else syn1
    2.44 -      }
    2.45 +    def syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
    2.46    }
    2.47  
    2.48    private def require_thys(initiators: List[Document.Node.Name],
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 21 14:54:29 2012 +0200
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 21 16:56:18 2012 +0200
     3.3 @@ -150,7 +150,9 @@
     3.4  
     3.5      val syntax =
     3.6        if (previous.is_init || updated_keywords)
     3.7 -        (base_syntax /: nodes.entries) { case (syn, (_, node)) => syn.add_keywords(node.header) }
     3.8 +        (base_syntax /: nodes.entries) {
     3.9 +          case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
    3.10 +        }
    3.11        else previous.syntax
    3.12  
    3.13      val reparse =