more uniform header_keywords in ML/Scala;
authorwenzelm
Wed Nov 05 21:59:21 2014 +0100 (2014-11-05)
changeset 589070ee3563803c9
parent 58906 29788e989d61
child 58908 58bedbc18915
more uniform header_keywords in ML/Scala;
tuned signature;
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Wed Nov 05 21:21:15 2014 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Wed Nov 05 21:59:21 2014 +0100
     1.3 @@ -72,8 +72,6 @@
     1.4    object Keywords
     1.5    {
     1.6      def empty: Keywords = new Keywords()
     1.7 -
     1.8 -    def apply(keywords: List[String]): Keywords = (empty /: keywords)(_ + _)
     1.9    }
    1.10  
    1.11    class Keywords private(
    1.12 @@ -99,9 +97,8 @@
    1.13  
    1.14      /* add keywords */
    1.15  
    1.16 -    def + (name: String): Keywords =
    1.17 -      new Keywords(minor + name, major, commands)
    1.18 -
    1.19 +    def + (name: String): Keywords = new Keywords(minor + name, major, commands)
    1.20 +    def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
    1.21      def + (name: String, kind: (String, List[String])): Keywords =
    1.22      {
    1.23        val major1 = major + name
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 21:21:15 2014 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 21:59:21 2014 +0100
     2.3 @@ -86,6 +86,8 @@
     2.4  
     2.5    /* add keywords */
     2.6  
     2.7 +  def + (name: String): Outer_Syntax = this + (name, None, None)
     2.8 +  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
     2.9    def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
    2.10      : Outer_Syntax =
    2.11    {
    2.12 @@ -99,8 +101,6 @@
    2.13        else completion + (name, replace getOrElse name)
    2.14      new Outer_Syntax(keywords1, completion1, language_context, true)
    2.15    }
    2.16 -  def + (name: String): Outer_Syntax = this + (name, None, None)
    2.17 -  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
    2.18  
    2.19    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    2.20      (this /: keywords) {
     3.1 --- a/src/Pure/Thy/thy_header.ML	Wed Nov 05 21:21:15 2014 +0100
     3.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Nov 05 21:59:21 2014 +0100
     3.3 @@ -81,9 +81,13 @@
     3.4    Keyword.empty_keywords
     3.5    |> fold (Keyword.add o rpair NONE)
     3.6      ["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN]
     3.7 -  |> fold (Keyword.add o rpair (SOME Keyword.heading))
     3.8 -    [headerN, chapterN, sectionN, subsectionN, subsubsectionN]
     3.9 -  |> Keyword.add (theoryN, SOME Keyword.thy_begin);
    3.10 +  |> fold Keyword.add
    3.11 +    [(headerN, SOME Keyword.heading),
    3.12 +     (chapterN, SOME Keyword.heading),
    3.13 +     (sectionN, SOME Keyword.heading),
    3.14 +     (subsectionN, SOME Keyword.heading),
    3.15 +     (subsubsectionN, SOME Keyword.heading),
    3.16 +     (theoryN, SOME Keyword.thy_begin)];
    3.17  
    3.18  
    3.19  (* header args *)
     4.1 --- a/src/Pure/Thy/thy_header.scala	Wed Nov 05 21:21:15 2014 +0100
     4.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Nov 05 21:59:21 2014 +0100
     4.3 @@ -28,9 +28,14 @@
     4.4    val BEGIN = "begin"
     4.5  
     4.6    private val header_keywords =
     4.7 -    Keyword.Keywords(
     4.8 -      List("%", "(", ")", ",", "::", "==", AND, BEGIN,
     4.9 -        HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY))
    4.10 +    Keyword.Keywords.empty +
    4.11 +      "%" + "(" + ")" + "," + "::" + "==" + AND + BEGIN + IMPORTS + KEYWORDS +
    4.12 +      (HEADER, Keyword.HEADING) +
    4.13 +      (CHAPTER, Keyword.HEADING) +
    4.14 +      (SECTION, Keyword.HEADING) +
    4.15 +      (SUBSECTION, Keyword.HEADING) +
    4.16 +      (SUBSUBSECTION, Keyword.HEADING) +
    4.17 +      (THEORY, Keyword.THY_BEGIN)
    4.18  
    4.19  
    4.20    /* theory file name */
    4.21 @@ -81,14 +86,14 @@
    4.22        { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
    4.23  
    4.24      val heading =
    4.25 -      (keyword(HEADER) |
    4.26 -        keyword(CHAPTER) |
    4.27 -        keyword(SECTION) |
    4.28 -        keyword(SUBSECTION) |
    4.29 -        keyword(SUBSUBSECTION)) ~
    4.30 +      (command(HEADER) |
    4.31 +        command(CHAPTER) |
    4.32 +        command(SECTION) |
    4.33 +        command(SUBSECTION) |
    4.34 +        command(SUBSUBSECTION)) ~
    4.35        tags ~! document_source
    4.36  
    4.37 -    (rep(heading) ~ keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
    4.38 +    (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
    4.39    }
    4.40  
    4.41