clarified signature;
authorwenzelm
Wed Aug 29 12:44:17 2018 +0200 (14 months ago)
changeset 68841252b43600737
parent 68840 51ab4c78235b
child 68842 72c4452f4b94
clarified signature;
src/Pure/System/options.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/System/options.scala	Wed Aug 29 12:21:59 2018 +0200
     1.2 +++ b/src/Pure/System/options.scala	Wed Aug 29 12:44:17 2018 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4        atom("option value", tok => tok.is_name || tok.is_float)
     1.5    }
     1.6  
     1.7 -  object Parser extends Parse.Parser with Parser
     1.8 +  private object Parser extends Parser
     1.9    {
    1.10      def comment_marker: Parser[String] =
    1.11        $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded)
     2.1 --- a/src/Pure/Thy/sessions.scala	Wed Aug 29 12:21:59 2018 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Wed Aug 29 12:44:17 2018 +0200
     2.3 @@ -781,7 +781,7 @@
     2.4        theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
     2.5    }
     2.6  
     2.7 -  private object Parser extends Parse.Parser with Options.Parser
     2.8 +  private object Parser extends Options.Parser
     2.9    {
    2.10      private val chapter: Parser[Chapter] =
    2.11      {
     3.1 --- a/src/Pure/Thy/thy_header.scala	Wed Aug 29 12:21:59 2018 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Aug 29 12:44:17 2018 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4  import scala.util.matching.Regex
     3.5  
     3.6  
     3.7 -object Thy_Header extends Parse.Parser
     3.8 +object Thy_Header
     3.9  {
    3.10    /* bootstrap keywords */
    3.11  
    3.12 @@ -116,62 +116,65 @@
    3.13      bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
    3.14  
    3.15  
    3.16 -  /* header */
    3.17 +  /* parser */
    3.18  
    3.19 -  val header: Parser[Thy_Header] =
    3.20 +  trait Parser extends Parse.Parser
    3.21    {
    3.22 -    val opt_files =
    3.23 -      $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
    3.24 -      success(Nil)
    3.25 -
    3.26 -    val keyword_spec =
    3.27 -      atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    3.28 -      { case x ~ y ~ z => Keyword.Spec(x, y, z) }
    3.29 +    val header: Parser[Thy_Header] =
    3.30 +    {
    3.31 +      val opt_files =
    3.32 +        $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
    3.33 +        success(Nil)
    3.34  
    3.35 -    val keyword_decl =
    3.36 -      rep1(string) ~
    3.37 -      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
    3.38 -      { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) }
    3.39 +      val keyword_spec =
    3.40 +        atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    3.41 +        { case x ~ y ~ z => Keyword.Spec(x, y, z) }
    3.42  
    3.43 -    val keyword_decls =
    3.44 -      keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    3.45 -      { case xs ~ yss => (xs :: yss).flatten }
    3.46 +      val keyword_decl =
    3.47 +        rep1(string) ~
    3.48 +        opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
    3.49 +        { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) }
    3.50  
    3.51 -    val abbrevs =
    3.52 -      rep1sep(rep1(text) ~ ($$$("=") ~! rep1(text)), $$$("and")) ^^
    3.53 -        { case res => for ((as ~ (_ ~ bs)) <- res; a <- as; b <- bs) yield (a, b) }
    3.54 +      val keyword_decls =
    3.55 +        keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    3.56 +        { case xs ~ yss => (xs :: yss).flatten }
    3.57 +
    3.58 +      val abbrevs =
    3.59 +        rep1sep(rep1(text) ~ ($$$("=") ~! rep1(text)), $$$("and")) ^^
    3.60 +          { case res => for ((as ~ (_ ~ bs)) <- res; a <- as; b <- bs) yield (a, b) }
    3.61  
    3.62 -    val args =
    3.63 -      position(theory_name) ~
    3.64 -      (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
    3.65 -        { case None => Nil case Some(_ ~ xs) => xs }) ~
    3.66 -      (opt($$$(KEYWORDS) ~! keyword_decls) ^^
    3.67 -        { case None => Nil case Some(_ ~ xs) => xs }) ~
    3.68 -      (opt($$$(ABBREVS) ~! abbrevs) ^^
    3.69 -        { case None => Nil case Some(_ ~ xs) => xs }) ~
    3.70 -      $$$(BEGIN) ^^
    3.71 -      { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ =>
    3.72 -          val f = Symbol.decode _
    3.73 -          Thy_Header((f(name), pos),
    3.74 -            imports.map({ case (a, b) => (f(a), b) }),
    3.75 -            keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
    3.76 -              (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
    3.77 -            abbrevs.map({ case (a, b) => (f(a), f(b)) }))
    3.78 -      }
    3.79 +      val args =
    3.80 +        position(theory_name) ~
    3.81 +        (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
    3.82 +          { case None => Nil case Some(_ ~ xs) => xs }) ~
    3.83 +        (opt($$$(KEYWORDS) ~! keyword_decls) ^^
    3.84 +          { case None => Nil case Some(_ ~ xs) => xs }) ~
    3.85 +        (opt($$$(ABBREVS) ~! abbrevs) ^^
    3.86 +          { case None => Nil case Some(_ ~ xs) => xs }) ~
    3.87 +        $$$(BEGIN) ^^
    3.88 +        { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ =>
    3.89 +            val f = Symbol.decode _
    3.90 +            Thy_Header((f(name), pos),
    3.91 +              imports.map({ case (a, b) => (f(a), b) }),
    3.92 +              keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
    3.93 +                (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
    3.94 +              abbrevs.map({ case (a, b) => (f(a), f(b)) }))
    3.95 +        }
    3.96  
    3.97 -    val heading =
    3.98 -      (command(CHAPTER) |
    3.99 -        command(SECTION) |
   3.100 -        command(SUBSECTION) |
   3.101 -        command(SUBSUBSECTION) |
   3.102 -        command(PARAGRAPH) |
   3.103 -        command(SUBPARAGRAPH) |
   3.104 -        command(TEXT) |
   3.105 -        command(TXT) |
   3.106 -        command(TEXT_RAW)) ~
   3.107 -      tags ~! document_source
   3.108 +      val heading =
   3.109 +        (command(CHAPTER) |
   3.110 +          command(SECTION) |
   3.111 +          command(SUBSECTION) |
   3.112 +          command(SUBSUBSECTION) |
   3.113 +          command(PARAGRAPH) |
   3.114 +          command(SUBPARAGRAPH) |
   3.115 +          command(TEXT) |
   3.116 +          command(TXT) |
   3.117 +          command(TEXT_RAW)) ~
   3.118 +        tags ~! document_source
   3.119  
   3.120 -    (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   3.121 +      (rep(heading) ~ command(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   3.122 +    }
   3.123    }
   3.124  
   3.125  
   3.126 @@ -198,6 +201,15 @@
   3.127      (drop_tokens, tokens1 ::: tokens2)
   3.128    }
   3.129  
   3.130 +  private object Parser extends Parser
   3.131 +  {
   3.132 +    def parse_header(tokens: List[Token], pos: Token.Pos): Thy_Header =
   3.133 +      parse(commit(header), Token.reader(tokens, pos)) match {
   3.134 +        case Success(result, _) => result
   3.135 +        case bad => error(bad.toString)
   3.136 +      }
   3.137 +  }
   3.138 +
   3.139    def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
   3.140    {
   3.141      val (_, tokens0) = read_tokens(reader, true)
   3.142 @@ -206,10 +218,7 @@
   3.143      val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
   3.144      val pos = (start /: drop_tokens)(_.advance(_))
   3.145  
   3.146 -    parse(commit(header), Token.reader(tokens, pos)) match {
   3.147 -      case Success(result, _) => result
   3.148 -      case bad => error(bad.toString)
   3.149 -    }
   3.150 +    Parser.parse_header(tokens, pos)
   3.151    }
   3.152  }
   3.153