--- 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
--- 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;
--- 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 */
--- 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) }
}
--- 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
--- 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 =
--- 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) }