more explicit types;
authorwenzelm
Tue Apr 04 22:56:28 2017 +0200 (2017-04-04)
changeset 6538436255c43c64c
parent 65383 089f2edefb77
child 65385 23f36ab9042b
more explicit types;
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/protocol.scala
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Tue Apr 04 22:53:01 2017 +0200
     1.2 +++ b/src/Pure/Isar/keyword.scala	Tue Apr 04 22:56:28 2017 +0200
     1.3 @@ -93,11 +93,14 @@
     1.4  
     1.5    /** keyword tables **/
     1.6  
     1.7 -  type Spec = ((String, List[String]), List[String])
     1.8 -
     1.9 -  val no_spec: Spec = (("", Nil), Nil)
    1.10 -  val before_command_spec: Spec = ((BEFORE_COMMAND, Nil), Nil)
    1.11 -  val quasi_command_spec: Spec = ((QUASI_COMMAND, Nil), Nil)
    1.12 +  object Spec
    1.13 +  {
    1.14 +    val none: Spec = Spec("")
    1.15 +  }
    1.16 +  sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
    1.17 +  {
    1.18 +    def is_none: Boolean = kind == ""
    1.19 +  }
    1.20  
    1.21    object Keywords
    1.22    {
    1.23 @@ -165,9 +168,13 @@
    1.24  
    1.25      def add_keywords(header: Thy_Header.Keywords): Keywords =
    1.26        (this /: header) {
    1.27 -        case (keywords, (name, ((kind, exts), _))) =>
    1.28 -          if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
    1.29 -          else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
    1.30 +        case (keywords, (name, spec)) =>
    1.31 +          if (spec.is_none)
    1.32 +            keywords + Symbol.decode(name) + Symbol.encode(name)
    1.33 +          else
    1.34 +            keywords +
    1.35 +              (Symbol.decode(name), spec.kind, spec.exts) +
    1.36 +              (Symbol.encode(name), spec.kind, spec.exts)
    1.37        }
    1.38  
    1.39  
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Apr 04 22:53:01 2017 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Apr 04 22:56:28 2017 +0200
     2.3 @@ -71,8 +71,10 @@
     2.4  
     2.5    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
     2.6      (this /: keywords) {
     2.7 -      case (syntax, (name, ((kind, exts), _))) =>
     2.8 -        syntax + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
     2.9 +      case (syntax, (name, spec)) =>
    2.10 +        syntax +
    2.11 +          (Symbol.decode(name), spec.kind, spec.exts) +
    2.12 +          (Symbol.encode(name), spec.kind, spec.exts)
    2.13      }
    2.14  
    2.15  
     3.1 --- a/src/Pure/PIDE/protocol.scala	Tue Apr 04 22:53:01 2017 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Apr 04 22:56:28 2017 +0200
     3.3 @@ -361,10 +361,12 @@
     3.4                val master_dir = File.standard_url(name.master_dir)
     3.5                val theory = Long_Name.base_name(name.theory)
     3.6                val imports = header.imports.map({ case (a, _) => a.node })
     3.7 +              val keywords =
     3.8 +                header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
     3.9                (Nil,
    3.10                  pair(string, pair(string, pair(list(string), pair(list(pair(string,
    3.11                      pair(pair(string, list(string)), list(string)))), list(string)))))(
    3.12 -                (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
    3.13 +                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
    3.14            { case Document.Node.Perspective(a, b, c) =>
    3.15                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
    3.16                  list(pair(id, pair(string, list(string))))(c.dest)) }))
     4.1 --- a/src/Pure/Thy/thy_header.scala	Tue Apr 04 22:53:01 2017 +0200
     4.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Apr 04 22:56:28 2017 +0200
     4.3 @@ -39,28 +39,28 @@
     4.4  
     4.5    val bootstrap_header: Keywords =
     4.6      List(
     4.7 -      ("%", Keyword.no_spec),
     4.8 -      ("(", Keyword.no_spec),
     4.9 -      (")", Keyword.no_spec),
    4.10 -      (",", Keyword.no_spec),
    4.11 -      ("::", Keyword.no_spec),
    4.12 -      ("=", Keyword.no_spec),
    4.13 -      (AND, Keyword.no_spec),
    4.14 -      (BEGIN, Keyword.quasi_command_spec),
    4.15 -      (IMPORTS, Keyword.quasi_command_spec),
    4.16 -      (KEYWORDS, Keyword.quasi_command_spec),
    4.17 -      (ABBREVS, Keyword.quasi_command_spec),
    4.18 -      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    4.19 -      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    4.20 -      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    4.21 -      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    4.22 -      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    4.23 -      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
    4.24 -      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
    4.25 -      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
    4.26 -      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil))),
    4.27 -      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory"))),
    4.28 -      ("ML", ((Keyword.THY_DECL, Nil), List("ML"))))
    4.29 +      ("%", Keyword.Spec.none),
    4.30 +      ("(", Keyword.Spec.none),
    4.31 +      (")", Keyword.Spec.none),
    4.32 +      (",", Keyword.Spec.none),
    4.33 +      ("::", Keyword.Spec.none),
    4.34 +      ("=", Keyword.Spec.none),
    4.35 +      (AND, Keyword.Spec.none),
    4.36 +      (BEGIN, Keyword.Spec(Keyword.QUASI_COMMAND)),
    4.37 +      (IMPORTS, Keyword.Spec(Keyword.QUASI_COMMAND)),
    4.38 +      (KEYWORDS, Keyword.Spec(Keyword.QUASI_COMMAND)),
    4.39 +      (ABBREVS, Keyword.Spec(Keyword.QUASI_COMMAND)),
    4.40 +      (CHAPTER, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    4.41 +      (SECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    4.42 +      (SUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    4.43 +      (SUBSUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    4.44 +      (PARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    4.45 +      (SUBPARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)),
    4.46 +      (TEXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
    4.47 +      (TXT, Keyword.Spec(Keyword.DOCUMENT_BODY)),
    4.48 +      (TEXT_RAW, Keyword.Spec(Keyword.DOCUMENT_RAW)),
    4.49 +      (THEORY, Keyword.Spec(Keyword.THY_BEGIN, tags = List("theory"))),
    4.50 +      ("ML", Keyword.Spec(Keyword.THY_DECL, tags = List("ML"))))
    4.51  
    4.52    private val bootstrap_keywords =
    4.53      Keyword.Keywords.empty.add_keywords(bootstrap_header)
    4.54 @@ -114,12 +114,12 @@
    4.55  
    4.56      val keyword_spec =
    4.57        atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    4.58 -      { case x ~ y ~ z => ((x, y), z) }
    4.59 +      { case x ~ y ~ z => Keyword.Spec(x, y, z) }
    4.60  
    4.61      val keyword_decl =
    4.62        rep1(string) ~
    4.63        opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
    4.64 -      { case xs ~ y => xs.map((_, y.getOrElse(Keyword.no_spec))) }
    4.65 +      { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) }
    4.66  
    4.67      val keyword_decls =
    4.68        keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    4.69 @@ -192,7 +192,8 @@
    4.70      val f = Symbol.decode _
    4.71      Thy_Header((f(name._1), name._2),
    4.72        imports.map({ case (a, b) => (f(a), b) }),
    4.73 -      keywords.map({ case (a, ((b, c), d)) => (f(a), ((f(b), c.map(f)), d.map(f))) }),
    4.74 +      keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
    4.75 +        (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
    4.76        abbrevs.map({ case (a, b) => (f(a), f(b)) }))
    4.77    }
    4.78  }