tuned signature;
authorwenzelm
Wed Nov 05 22:17:05 2014 +0100 (2014-11-05)
changeset 5890858bedbc18915
parent 58907 0ee3563803c9
child 58909 f323497583d1
tuned signature;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse.scala
src/Pure/System/options.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 21:59:21 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 22:17:05 2014 +0100
     1.3 @@ -196,7 +196,7 @@
     1.4  local
     1.5  
     1.6  fun parse_command syntax =
     1.7 -  Parse.position Parse.command :|-- (fn (name, pos) =>
     1.8 +  Parse.position Parse.command_ :|-- (fn (name, pos) =>
     1.9      let
    1.10        val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
    1.11      in
     2.1 --- a/src/Pure/Isar/parse.ML	Wed Nov 05 21:59:21 2014 +0100
     2.2 +++ b/src/Pure/Isar/parse.ML	Wed Nov 05 22:17:05 2014 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4    val position: 'a parser -> ('a * Position.T) parser
     2.5    val source_position: 'a parser -> Symbol_Pos.source parser
     2.6    val inner_syntax: 'a parser -> string parser
     2.7 -  val command: string parser
     2.8 +  val command_: string parser
     2.9    val keyword: string parser
    2.10    val short_ident: string parser
    2.11    val long_ident: string parser
    2.12 @@ -33,7 +33,7 @@
    2.13    val verbatim: string parser
    2.14    val cartouche: string parser
    2.15    val eof: string parser
    2.16 -  val command_name: string -> string parser
    2.17 +  val command: string -> string parser
    2.18    val keyword_with: (string -> bool) -> string parser
    2.19    val keyword_markup: bool * Markup.T -> string -> string parser
    2.20    val keyword_improper: string -> string parser
    2.21 @@ -180,7 +180,7 @@
    2.22    group (fn () => Token.str_of_kind k)
    2.23      (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
    2.24  
    2.25 -val command = kind Token.Command;
    2.26 +val command_ = kind Token.Command;
    2.27  val keyword = kind Token.Keyword;
    2.28  val short_ident = kind Token.Ident;
    2.29  val long_ident = kind Token.LongIdent;
    2.30 @@ -196,7 +196,7 @@
    2.31  val cartouche = kind Token.Cartouche;
    2.32  val eof = kind Token.EOF;
    2.33  
    2.34 -fun command_name x =
    2.35 +fun command x =
    2.36    group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
    2.37      (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
    2.38    >> Token.content_of;
     3.1 --- a/src/Pure/Isar/parse.scala	Wed Nov 05 21:59:21 2014 +0100
     3.2 +++ b/src/Pure/Isar/parse.scala	Wed Nov 05 22:17:05 2014 +0100
     3.3 @@ -51,7 +51,7 @@
     3.4        token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
     3.5          { case (_, pos) => pos.position }
     3.6  
     3.7 -    def keyword(name: String): Parser[String] =
     3.8 +    def $$$(name: String): Parser[String] =
     3.9        atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
    3.10  
    3.11      def string: Parser[String] = atom("string", _.is_string)
    3.12 @@ -73,7 +73,7 @@
    3.13            tok.kind == Token.Kind.IDENT ||
    3.14            tok.kind == Token.Kind.STRING)
    3.15  
    3.16 -    def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
    3.17 +    def tags: Parser[List[String]] = rep($$$("%") ~> tag_name)
    3.18  
    3.19  
    3.20      /* wrappers */
     4.1 --- a/src/Pure/System/options.scala	Wed Nov 05 21:59:21 2014 +0100
     4.2 +++ b/src/Pure/System/options.scala	Wed Nov 05 22:17:05 2014 +0100
     4.3 @@ -93,15 +93,15 @@
     4.4      {
     4.5        command(SECTION) ~! text ^^
     4.6          { case _ ~ a => (options: Options) => options.set_section(a) } |
     4.7 -      opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
     4.8 -      keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
     4.9 +      opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ $$$(":") ~ option_type ~
    4.10 +      $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    4.11          { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
    4.12              (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
    4.13      }
    4.14  
    4.15      val prefs_entry: Parser[Options => Options] =
    4.16      {
    4.17 -      option_name ~ (keyword("=") ~! option_value) ^^
    4.18 +      option_name ~ ($$$("=") ~! option_value) ^^
    4.19        { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
    4.20      }
    4.21  
     5.1 --- a/src/Pure/Thy/thy_header.ML	Wed Nov 05 21:59:21 2014 +0100
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Nov 05 22:17:05 2014 +0100
     5.3 @@ -131,15 +131,15 @@
     5.4  (* read header *)
     5.5  
     5.6  val heading =
     5.7 -  (Parse.command_name headerN ||
     5.8 -    Parse.command_name chapterN ||
     5.9 -    Parse.command_name sectionN ||
    5.10 -    Parse.command_name subsectionN ||
    5.11 -    Parse.command_name subsubsectionN) --
    5.12 +  (Parse.command headerN ||
    5.13 +    Parse.command chapterN ||
    5.14 +    Parse.command sectionN ||
    5.15 +    Parse.command subsectionN ||
    5.16 +    Parse.command subsubsectionN) --
    5.17    Parse.tags -- Parse.!!! Parse.document_source;
    5.18  
    5.19  val header =
    5.20 -  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
    5.21 +  (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
    5.22  
    5.23  fun token_source pos str =
    5.24    str
     6.1 --- a/src/Pure/Thy/thy_header.scala	Wed Nov 05 21:59:21 2014 +0100
     6.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Nov 05 22:17:05 2014 +0100
     6.3 @@ -57,7 +57,7 @@
     6.4      val file_name = atom("file name", _.is_name)
     6.5  
     6.6      val opt_files =
     6.7 -      keyword("(") ~! (rep1sep(name, keyword(",")) <~ keyword(")")) ^^ { case _ ~ x => x } |
     6.8 +      $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
     6.9        success(Nil)
    6.10      val keyword_spec =
    6.11        atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    6.12 @@ -65,24 +65,24 @@
    6.13  
    6.14      val keyword_decl =
    6.15        rep1(string) ~
    6.16 -      opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    6.17 -      opt(keyword("==") ~! name ^^ { case _ ~ x => x }) ^^
    6.18 +      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    6.19 +      opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
    6.20        { case xs ~ y ~ z => xs.map((_, y, z)) }
    6.21      val keyword_decls =
    6.22 -      keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    6.23 +      keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    6.24        { case xs ~ yss => (xs :: yss).flatten }
    6.25  
    6.26      val file =
    6.27 -      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    6.28 +      $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    6.29        file_name ^^ (x => (x, true))
    6.30  
    6.31      val args =
    6.32        theory_name ~
    6.33 -      (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^
    6.34 +      (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^
    6.35          { case None => Nil case Some(_ ~ xs) => xs }) ~
    6.36 -      (opt(keyword(KEYWORDS) ~! keyword_decls) ^^
    6.37 +      (opt($$$(KEYWORDS) ~! keyword_decls) ^^
    6.38          { case None => Nil case Some(_ ~ xs) => xs }) ~
    6.39 -      keyword(BEGIN) ^^
    6.40 +      $$$(BEGIN) ^^
    6.41        { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
    6.42  
    6.43      val heading =
     7.1 --- a/src/Pure/Tools/build.scala	Wed Nov 05 21:59:21 2014 +0100
     7.2 +++ b/src/Pure/Tools/build.scala	Wed Nov 05 22:17:05 2014 +0100
     7.3 @@ -228,30 +228,30 @@
     7.4        val session_name = atom("session name", _.is_name)
     7.5  
     7.6        val option =
     7.7 -        name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
     7.8 -      val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
     7.9 +        name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
    7.10 +      val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
    7.11  
    7.12        val theories =
    7.13 -        (keyword(GLOBAL_THEORIES) | keyword(THEORIES)) ~!
    7.14 +        ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
    7.15            ((options | success(Nil)) ~ rep(theory_xname)) ^^
    7.16            { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
    7.17  
    7.18        val document_files =
    7.19 -        keyword(DOCUMENT_FILES) ~!
    7.20 -          ((keyword("(") ~! (keyword(IN) ~! (path ~ keyword(")"))) ^^
    7.21 +        $$$(DOCUMENT_FILES) ~!
    7.22 +          (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
    7.23                { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
    7.24              rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
    7.25  
    7.26        command(SESSION) ~!
    7.27          (session_name ~
    7.28 -          ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
    7.29 -          ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
    7.30 -          (keyword("=") ~!
    7.31 -            (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
    7.32 -              ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
    7.33 -              ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    7.34 +          (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
    7.35 +          (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
    7.36 +          ($$$("=") ~!
    7.37 +            (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
    7.38 +              (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
    7.39 +              (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    7.40                rep1(theories) ~
    7.41 -              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
    7.42 +              (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
    7.43                (rep(document_files) ^^ (x => x.flatten))))) ^^
    7.44          { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    7.45              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }