# HG changeset patch # User wenzelm # Date 1415222225 -3600 # Node ID 58bedbc189155aaaba97e37a50b0bd72de3c7b84 # Parent 0ee3563803c9dbd501ff394dd96bc88808656350 tuned signature; diff -r 0ee3563803c9 -r 58bedbc18915 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Wed Nov 05 21:59:21 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Wed Nov 05 22:17:05 2014 +0100 @@ -196,7 +196,7 @@ local fun parse_command syntax = - Parse.position Parse.command :|-- (fn (name, pos) => + Parse.position Parse.command_ :|-- (fn (name, pos) => let val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos; in diff -r 0ee3563803c9 -r 58bedbc18915 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Wed Nov 05 21:59:21 2014 +0100 +++ b/src/Pure/Isar/parse.ML Wed Nov 05 22:17:05 2014 +0100 @@ -17,7 +17,7 @@ val position: 'a parser -> ('a * Position.T) parser val source_position: 'a parser -> Symbol_Pos.source parser val inner_syntax: 'a parser -> string parser - val command: string parser + val command_: string parser val keyword: string parser val short_ident: string parser val long_ident: string parser @@ -33,7 +33,7 @@ val verbatim: string parser val cartouche: string parser val eof: string parser - val command_name: string -> string parser + val command: string -> string parser val keyword_with: (string -> bool) -> string parser val keyword_markup: bool * Markup.T -> string -> string parser val keyword_improper: string -> string parser @@ -180,7 +180,7 @@ group (fn () => Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of)); -val command = kind Token.Command; +val command_ = kind Token.Command; val keyword = kind Token.Keyword; val short_ident = kind Token.Ident; val long_ident = kind Token.LongIdent; @@ -196,7 +196,7 @@ val cartouche = kind Token.Cartouche; val eof = kind Token.EOF; -fun command_name x = +fun command x = group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x) (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x))) >> Token.content_of; diff -r 0ee3563803c9 -r 58bedbc18915 src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Wed Nov 05 21:59:21 2014 +0100 +++ b/src/Pure/Isar/parse.scala Wed Nov 05 22:17:05 2014 +0100 @@ -51,7 +51,7 @@ token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^ { case (_, pos) => pos.position } - def keyword(name: String): Parser[String] = + def $$$(name: String): Parser[String] = atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name) def string: Parser[String] = atom("string", _.is_string) @@ -73,7 +73,7 @@ tok.kind == Token.Kind.IDENT || tok.kind == Token.Kind.STRING) - def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name) + def tags: Parser[List[String]] = rep($$$("%") ~> tag_name) /* wrappers */ diff -r 0ee3563803c9 -r 58bedbc18915 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Wed Nov 05 21:59:21 2014 +0100 +++ b/src/Pure/System/options.scala Wed Nov 05 22:17:05 2014 +0100 @@ -93,15 +93,15 @@ { command(SECTION) ~! text ^^ { case _ ~ a => (options: Options) => options.set_section(a) } | - opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~ - keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^ + opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ $$$(":") ~ option_type ~ + $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^ { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) => (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) } } val prefs_entry: Parser[Options => Options] = { - option_name ~ (keyword("=") ~! option_value) ^^ + option_name ~ ($$$("=") ~! option_value) ^^ { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) } } diff -r 0ee3563803c9 -r 58bedbc18915 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Wed Nov 05 21:59:21 2014 +0100 +++ b/src/Pure/Thy/thy_header.ML Wed Nov 05 22:17:05 2014 +0100 @@ -131,15 +131,15 @@ (* read header *) val heading = - (Parse.command_name headerN || - Parse.command_name chapterN || - Parse.command_name sectionN || - Parse.command_name subsectionN || - Parse.command_name subsubsectionN) -- + (Parse.command headerN || + Parse.command chapterN || + Parse.command sectionN || + Parse.command subsectionN || + Parse.command subsubsectionN) -- Parse.tags -- Parse.!!! Parse.document_source; val header = - (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args; + (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args; fun token_source pos str = str diff -r 0ee3563803c9 -r 58bedbc18915 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Wed Nov 05 21:59:21 2014 +0100 +++ b/src/Pure/Thy/thy_header.scala Wed Nov 05 22:17:05 2014 +0100 @@ -57,7 +57,7 @@ val file_name = atom("file name", _.is_name) val opt_files = - keyword("(") ~! (rep1sep(name, keyword(",")) <~ keyword(")")) ^^ { case _ ~ x => x } | + $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } | success(Nil) val keyword_spec = atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^ @@ -65,24 +65,24 @@ val keyword_decl = rep1(string) ~ - opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~ - opt(keyword("==") ~! name ^^ { case _ ~ x => x }) ^^ + opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~ + opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^ { case xs ~ y ~ z => xs.map((_, y, z)) } val keyword_decls = - keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ + keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ { case xs ~ yss => (xs :: yss).flatten } val file = - keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | + $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | file_name ^^ (x => (x, true)) val args = theory_name ~ - (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^ + (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ - (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ + (opt($$$(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ - keyword(BEGIN) ^^ + $$$(BEGIN) ^^ { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) } val heading = diff -r 0ee3563803c9 -r 58bedbc18915 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Nov 05 21:59:21 2014 +0100 +++ b/src/Pure/Tools/build.scala Wed Nov 05 22:17:05 2014 +0100 @@ -228,30 +228,30 @@ val session_name = atom("session name", _.is_name) val option = - name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } - val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]") + name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } + val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]") val theories = - (keyword(GLOBAL_THEORIES) | keyword(THEORIES)) ~! + ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~! ((options | success(Nil)) ~ rep(theory_xname)) ^^ { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) } val document_files = - keyword(DOCUMENT_FILES) ~! - ((keyword("(") ~! (keyword(IN) ~! (path ~ keyword(")"))) ^^ + $$$(DOCUMENT_FILES) ~! + (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^ { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) } command(SESSION) ~! (session_name ~ - ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~ - ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~ - (keyword("=") ~! - (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~ - ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~ - ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ + (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~ + (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~ + ($$$("=") ~! + (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ + (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~ + (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ rep1(theories) ~ - ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~ + (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~ (rep(document_files) ^^ (x => x.flatten))))) ^^ { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) => Session_Entry(pos, a, b, c, d, e, f, g, h, i) }