# 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) }