src/Pure/Thy/thy_header.scala
changeset 58908 58bedbc18915
parent 58907 0ee3563803c9
child 58928 23d0ffd48006
     1.1 --- a/src/Pure/Thy/thy_header.scala	Wed Nov 05 21:59:21 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Nov 05 22:17:05 2014 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4      val file_name = atom("file name", _.is_name)
     1.5  
     1.6      val opt_files =
     1.7 -      keyword("(") ~! (rep1sep(name, keyword(",")) <~ keyword(")")) ^^ { case _ ~ x => x } |
     1.8 +      $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
     1.9        success(Nil)
    1.10      val keyword_spec =
    1.11        atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
    1.12 @@ -65,24 +65,24 @@
    1.13  
    1.14      val keyword_decl =
    1.15        rep1(string) ~
    1.16 -      opt(keyword("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    1.17 -      opt(keyword("==") ~! name ^^ { case _ ~ x => x }) ^^
    1.18 +      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
    1.19 +      opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
    1.20        { case xs ~ y ~ z => xs.map((_, y, z)) }
    1.21      val keyword_decls =
    1.22 -      keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    1.23 +      keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
    1.24        { case xs ~ yss => (xs :: yss).flatten }
    1.25  
    1.26      val file =
    1.27 -      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    1.28 +      $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    1.29        file_name ^^ (x => (x, true))
    1.30  
    1.31      val args =
    1.32        theory_name ~
    1.33 -      (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^
    1.34 +      (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^
    1.35          { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.36 -      (opt(keyword(KEYWORDS) ~! keyword_decls) ^^
    1.37 +      (opt($$$(KEYWORDS) ~! keyword_decls) ^^
    1.38          { case None => Nil case Some(_ ~ xs) => xs }) ~
    1.39 -      keyword(BEGIN) ^^
    1.40 +      $$$(BEGIN) ^^
    1.41        { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
    1.42  
    1.43      val heading =